---

Step * 1 of Lemma groupoid-left-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)) y z
6. b : cat-arrow(cat(G)) y z
7. c : cat-arrow(cat(G)) x y
8. (cat-comp(cat(G)) x y z c a) = (cat-comp(cat(G)) x y z c b) ∈ (cat-arrow(cat(G)) x z)
⊢ a = b ∈ (cat-arrow(cat(G)) y z)
BY
{ TACTIC:((ApFunToHypEquands `Z' ⌜cat-comp(cat(G)) y x z groupoid-inv(G;x;y;c) Z⌝ ⌜cat-arrow(cat(G)) y z⌝ (-1)⋅
           THENA Auto
           )
          THEN RWW "cat-comp-assoc< groupoid_inv.2 cat-comp-ident.1" (-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))  y  z
6.  b  :  cat-arrow(cat(G))  y  z
7.  c  :  cat-arrow(cat(G))  x  y
8.  (cat-comp(cat(G))  x  y  z  c  a)  =  (cat-comp(cat(G))  x  y  z  c  b)
\mvdash{}  a  =  b


By

---

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

---

Home Index