Nuprl Definition : trans-horizontal-comp
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
x |→ cat-comp(E) (J (F x)) (K (F x)) (K (G x)) (tJK (F x)) (K (F x) (G x) (tFG x))
Definitions occuring in Statement :
mk-nat-trans: x |→ T[x],
functor-arrow: arrow(F),
functor-ob: ob(F),
cat-comp: cat-comp(C),
apply: f a
Definitions occuring in definition :
mk-nat-trans: x |→ T[x],
cat-comp: cat-comp(C),
functor-arrow: arrow(F),
functor-ob: ob(F),
apply: f a
FDL editor aliases :
trans-horizontal-comp
Latex:
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
x |\mrightarrow{} cat-comp(E) (J (F x)) (K (F x)) (K (G x)) (tJK (F x)) (K (F x) (G x) (tFG x))
Date html generated:
2020_05_20-AM-07_54_20
Last ObjectModification:
2017_01_16-PM-02_53_17
Theory : small!categories
Home
Index