---

Step * of Lemma retraction-epic

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

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

---

Latex:

---

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


By

---

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

---

Home Index