Nuprl Definition : cat-initial
Initial(i) == ∀[x:cat-ob(C)]. ((∀[f,g:cat-arrow(C) i x]. (f = g ∈ (cat-arrow(C) i x))) ∧ (cat-arrow(C) i x))
Definitions occuring in Statement :
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
cat-ob: cat-ob(C),
and: P ∧ Q,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
apply: f a,
cat-arrow: cat-arrow(C)
FDL editor aliases :
cat-initial
Latex:
Initial(i) == \mforall{}[x:cat-ob(C)]. ((\mforall{}[f,g:cat-arrow(C) i x]. (f = g)) \mwedge{} (cat-arrow(C) i x))
Date html generated:
2020_05_20-AM-07_50_32
Last ObjectModification:
2017_01_09-AM-09_52_01
Theory : small!categories
Home
Index