---

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

---

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


By

---

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

---

Home Index