Nuprl Definition : cat-final
Final(fnl) == ∀[x:cat-ob(C)]. ((∀[f,g:cat-arrow(C) x fnl]. (f = g ∈ (cat-arrow(C) x fnl))) ∧ (cat-arrow(C) x fnl))
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-final
Latex:
Final(fnl) == \mforall{}[x:cat-ob(C)]. ((\mforall{}[f,g:cat-arrow(C) x fnl]. (f = g)) \mwedge{} (cat-arrow(C) x fnl))
Date html generated:
2020_05_20-AM-07_50_37
Last ObjectModification:
2017_01_09-AM-09_52_33
Theory : small!categories
Home
Index