Nuprl Definition : nat-trans
nat-trans(C;D;F;G) ==
{trans:A:cat-ob(C) ⟶ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) A))|
∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(G) B) (trans A) (functor-arrow(G) A B g))
= (cat-comp(D) (functor-ob(F) A) (functor-ob(F) B) (functor-ob(G) B) (functor-arrow(F) A B g) (trans B))
∈ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) B)))}
Definitions occuring in Statement :
functor-arrow: functor-arrow(F),
functor-ob: functor-ob(F),
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
cat-comp: cat-comp(C),
functor-ob: functor-ob(F),
functor-arrow: functor-arrow(F),
apply: f a
FDL editor aliases :
nat-trans
Latex:
nat-trans(C;D;F;G) ==
\{trans:A:cat-ob(C) {}\mrightarrow{} (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) A))|
\mforall{}A,B:cat-ob(C). \mforall{}g:cat-arrow(C) A B.
((cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(G) B) (trans A)
(functor-arrow(G) A B g))
= (cat-comp(D) (functor-ob(F) A) (functor-ob(F) B) (functor-ob(G) B) (functor-arrow(F) A B g)
(trans B)))\}
Date html generated:
2016_05_18-AM-11_52_28
Last ObjectModification:
2015_09_23-AM-09_29_09
Theory : small!categories
Home
Index