---

Step * 1 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)
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)
BY
{ (RWW  "cat-comp-assoc 6 cat-comp-ident.2" (-1) THEN Auto) }

---

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


By

---

Latex:
(RWW    "cat-comp-assoc  6  cat-comp-ident.2"  (-1)  THEN  Auto)

---

Home Index