---

Step * 1 of Lemma cat-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. g1 : cat-arrow(C) y x
7. fg1=1
8. fg2=1
9. h : cat-arrow(C) y x
10. hf=1
11. g1 = h ∈ (cat-arrow(C) y x)
12. g2 = h ∈ (cat-arrow(C) y x)
⊢ g1 = g2 ∈ (cat-arrow(C) y x)
BY
{ Eq }

---

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.  g1  :  cat-arrow(C)  y  x
7.  fg1=1
8.  fg2=1
9.  h  :  cat-arrow(C)  y  x
10.  hf=1
11.  g1  =  h
12.  g2  =  h
\mvdash{}  g1  =  g2


By

---

Latex:
Eq

---

Home Index