---

Step * 1 of Lemma left-right-inverse-unique


1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. f : cat-arrow(C) x y
5. g2 : cat-arrow(C) y x
6. g2f=1
7. g1 : cat-arrow(C) y x
8. fg1=1
⊢ g1 = g2 ∈ (cat-arrow(C) y x)
BY
{ All (Unfold `cat-inverse`) }

1
1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. f : cat-arrow(C) x y
5. g2 : cat-arrow(C) y x
6. (cat-comp(C) y x y g2 f) = (cat-id(C) y) ∈ (cat-arrow(C) y y)
7. g1 : cat-arrow(C) y x
8. (cat-comp(C) x y x f g1) = (cat-id(C) x) ∈ (cat-arrow(C) x x)
⊢ g1 = g2 ∈ (cat-arrow(C) y x)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  x  :  cat-ob(C)
3.  y  :  cat-ob(C)
4.  f  :  cat-arrow(C)  x  y
5.  g2  :  cat-arrow(C)  y  x
6.  g2f=1
7.  g1  :  cat-arrow(C)  y  x
8.  fg1=1
\mvdash{}  g1  =  g2


By

---

Latex:
All  (Unfold  `cat-inverse`)

---

Home Index