Nuprl Definition : cat-monic
monic(f) ==
∀[x:cat-ob(C)]. ∀[g,h:cat-arrow(C) x y].
g = h ∈ (cat-arrow(C) x y) supposing (cat-comp(C) x y z g f) = (cat-comp(C) x y z h f) ∈ (cat-arrow(C) x z)
Definitions occuring in Statement :
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
cat-ob: cat-ob(C),
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
cat-comp: cat-comp(C),
equal: s = t ∈ T,
apply: f a,
cat-arrow: cat-arrow(C)
FDL editor aliases :
cat-monic
Latex:
monic(f) ==
\mforall{}[x:cat-ob(C)]. \mforall{}[g,h:cat-arrow(C) x y].
g = h supposing (cat-comp(C) x y z g f) = (cat-comp(C) x y z h f)
Date html generated:
2020_05_20-AM-07_50_22
Last ObjectModification:
2017_01_08-PM-01_52_02
Theory : small!categories
Home
Index