Nuprl Definition : cat-epic
epic(f) ==
∀[z:cat-ob(C)]. ∀[g,h:cat-arrow(C) y z].
g = h ∈ (cat-arrow(C) y z) supposing (cat-comp(C) x y z f g) = (cat-comp(C) x y z f h) ∈ (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-epic
Latex:
epic(f) ==
\mforall{}[z:cat-ob(C)]. \mforall{}[g,h:cat-arrow(C) y z].
g = h supposing (cat-comp(C) x y z f g) = (cat-comp(C) x y z f h)
Date html generated:
2020_05_20-AM-07_50_27
Last ObjectModification:
2017_01_08-PM-01_54_53
Theory : small!categories
Home
Index