---

Step * 1 of Lemma retraction-epic


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)
BY
{ (ApFunToHypEquands  `arrow' ⌜cat-comp(C) y x z j arrow⌝ ⌜cat-arrow(C) y z⌝ (-1)⋅ THENA Auto) }

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)
11. (cat-comp(C) y x z j (cat-comp(C) x y z f g)) = (cat-comp(C) y x z j (cat-comp(C) x y z f h)) ∈ (cat-arrow(C) y z)
⊢ g = h ∈ (cat-arrow(C) y z)

---

Latex:

---

Latex:

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)
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)
\mvdash{}  g  =  h


By

---

Latex:
(ApFunToHypEquands    `arrow'  \mkleeneopen{}cat-comp(C)  y  x  z  j  arrow\mkleeneclose{}  \mkleeneopen{}cat-arrow(C)  y  z\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index