Nuprl Definition : identity-trans
identity-trans(C;D;F) == A |→ cat-id(D) (F A)
Definitions occuring in Statement :
mk-nat-trans: x |→ T[x],
functor-ob: ob(F),
cat-id: cat-id(C),
apply: f a
Definitions occuring in definition :
mk-nat-trans: x |→ T[x],
cat-id: cat-id(C),
apply: f a,
functor-ob: ob(F)
FDL editor aliases :
identity-trans
Latex:
identity-trans(C;D;F) == A |\mrightarrow{} cat-id(D) (F A)
Date html generated:
2020_05_20-AM-07_51_34
Last ObjectModification:
2017_01_10-PM-04_35_10
Theory : small!categories
Home
Index