Nuprl Definition : trans-comp
trans-comp(C;D;F;G;H;t1;t2) == A |→ cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(H) A) (t1 A) (t2 A)
Definitions occuring in Statement :
mk-nat-trans: x |→ T[x],
functor-ob: functor-ob(F),
cat-comp: cat-comp(C),
apply: f a
Definitions occuring in definition :
apply: f a,
functor-ob: functor-ob(F),
cat-comp: cat-comp(C),
mk-nat-trans: x |→ T[x]
FDL editor aliases :
trans-comp
Latex:
trans-comp(C;D;F;G;H;t1;t2) ==
A |\mrightarrow{} cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(H) A) (t1 A) (t2 A)
Date html generated:
2017_01_11-AM-09_18_15
Last ObjectModification:
2017_01_10-PM-04_37_14
Theory : small!categories
Home
Index