Nuprl Definition : trans-horizontal-comp
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
x |→ cat-comp(E) (ob(J) (ob(F) x)) (ob(K) (ob(F) x)) (ob(K) (ob(G) x)) (tJK (ob(F) x))
(arrow(K) (ob(F) x) (ob(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 :
apply: f a,
functor-ob: ob(F),
functor-arrow: arrow(F),
cat-comp: cat-comp(C),
mk-nat-trans: x |→ T[x]
FDL editor aliases :
trans-horizontal-comp
Latex:
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
x |\mrightarrow{} cat-comp(E) (ob(J) (ob(F) x)) (ob(K) (ob(F) x)) (ob(K) (ob(G) x)) (tJK (ob(F) x))
(arrow(K) (ob(F) x) (ob(G) x) (tFG x))
Date html generated:
2017_01_19-PM-02_54_14
Last ObjectModification:
2017_01_16-PM-02_53_17
Theory : small!categories
Home
Index