---

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
{ ((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:
((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