---

Step * 1 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. (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)
BY
{ ((InstLemma `cat-comp-assoc` [⌜C⌝;⌜y⌝;⌜x⌝;⌜y⌝;⌜x⌝;⌜g2⌝;⌜f⌝;⌜g1⌝]⋅
    THENM RWO "-2 -4" (-1)
    THENM RWO "cat-comp-ident.1 cat-comp-ident.2" (-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.  g2  :  cat-arrow(C)  y  x
6.  (cat-comp(C)  y  x  y  g2  f)  =  (cat-id(C)  y)
7.  g1  :  cat-arrow(C)  y  x
8.  (cat-comp(C)  x  y  x  f  g1)  =  (cat-id(C)  x)
\mvdash{}  g1  =  g2


By

---

Latex:
((InstLemma  `cat-comp-assoc`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}g2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g1\mkleeneclose{}]\mcdot{}
    THENM  RWO  "-2  -4"  (-1)
    THENM  RWO  "cat-comp-ident.1  cat-comp-ident.2"  (-1))
  THEN  Auto
  )

---

Home Index