Nuprl Definition : nat-trans
nat-trans(C;D;F;G) ==
{trans:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))|
∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(D) (F A) (G A) (G B) (trans A) (G A B g))
= (cat-comp(D) (F A) (F B) (G B) (F A B g) (trans B))
∈ (cat-arrow(D) (F A) (G B)))}
Definitions occuring in Statement :
functor-arrow: arrow(F),
functor-ob: 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: ob(F),
functor-arrow: 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) (F A) (G A))|
\mforall{}A,B:cat-ob(C). \mforall{}g:cat-arrow(C) A B.
((cat-comp(D) (F A) (G A) (G B) (trans A) (G A B g))
= (cat-comp(D) (F A) (F B) (G B) (F A B g) (trans B)))\}
Date html generated:
2020_05_20-AM-07_51_13
Last ObjectModification:
2015_09_23-AM-09_29_09
Theory : small!categories
Home
Index