---

Step * 1 of Lemma co-retraction-monic


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index