---

Step * 1 of Lemma groupoid-right-cancellation


1. G : Groupoid
2. x : cat-ob(cat(G))
3. y : cat-ob(cat(G))
4. z : cat-ob(cat(G))
5. a : cat-arrow(cat(G)) x y
6. b : cat-arrow(cat(G)) x y
7. c : cat-arrow(cat(G)) y z
8. (cat-comp(cat(G)) x y z a c) = (cat-comp(cat(G)) x y z b c) ∈ (cat-arrow(cat(G)) x z)
⊢ a = b ∈ (cat-arrow(cat(G)) x y)
BY
{ TACTIC:((ApFunToHypEquands `Z' ⌜cat-comp(cat(G)) x z y Z groupoid-inv(G;y;z;c)⌝ ⌜cat-arrow(cat(G)) x y⌝ (-1)⋅
           THENA Auto
           )
          THEN RWW "cat-comp-assoc groupoid_inv.1 cat-comp-ident.2" (-1)
          THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  x  :  cat-ob(cat(G))
3.  y  :  cat-ob(cat(G))
4.  z  :  cat-ob(cat(G))
5.  a  :  cat-arrow(cat(G))  x  y
6.  b  :  cat-arrow(cat(G))  x  y
7.  c  :  cat-arrow(cat(G))  y  z
8.  (cat-comp(cat(G))  x  y  z  a  c)  =  (cat-comp(cat(G))  x  y  z  b  c)
\mvdash{}  a  =  b


By

---

Latex:
TACTIC:((ApFunToHypEquands  `Z'  \mkleeneopen{}cat-comp(cat(G))  x  z  y  Z  groupoid-inv(G;y;z;c)\mkleeneclose{} 
                  \mkleeneopen{}cat-arrow(cat(G))  x  y\mkleeneclose{}  (-1)\mcdot{}
                  THENA  Auto
                  )
                THEN  RWW  "cat-comp-assoc  groupoid\_inv.1  cat-comp-ident.2"  (-1)
                THEN  Auto)

---

Home Index