---

Step * of Lemma co-retraction-monic

∀[C:SmallCategory]. ∀[y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y z].  monic(f) supposing co-retraction(f)
BY
{ (Intros THEN D 0 THEN Auto THEN D 5 THEN RenameVar `j' 5 THEN UnfoldTopAb 6) }

1
1. C : SmallCategory
2. y : cat-ob(C)
3. z : cat-ob(C)
4. f : cat-arrow(C) y z
5. j : cat-arrow(C) z y
6. (cat-comp(C) y z y f j) = (cat-id(C) y) ∈ (cat-arrow(C) y y)
7. x : cat-ob(C)
8. g : cat-arrow(C) x y
9. h : cat-arrow(C) x y
10. (cat-comp(C) x y z g f) = (cat-comp(C) x y z h f) ∈ (cat-arrow(C) x z)
⊢ g = h ∈ (cat-arrow(C) x y)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[y,z:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  y  z].    monic(f)  supposing  co-retraction(f)


By

---

Latex:
(Intros  THEN  D  0  THEN  Auto  THEN  D  5  THEN  RenameVar  `j'  5  THEN  UnfoldTopAb  6)

---

Home Index