---

Step * 1 of Lemma groupoid-square1_wf

.....set predicate..... 
1. G : Groupoid
2. x00 : cat-ob(cat(G))
3. x10 : cat-ob(cat(G))
4. x01 : cat-ob(cat(G))
5. x11 : cat-ob(cat(G))
6. a : cat-arrow(cat(G)) x00 x10
7. b : cat-arrow(cat(G)) x10 x11
8. c : cat-arrow(cat(G)) x00 x01
⊢ a o b = c o cat-comp(cat(G)) x01 x10 x11 (cat-comp(cat(G)) x01 x00 x10 groupoid-inv(G;x00;x01;c) a) b
BY
{ TACTIC:(Unfold `cat-square-commutes` 0
          THEN (RWW "cat-comp-assoc< groupoid-right-cancellation groupoid_inv.1 cat-comp-ident.1" 0⋅ THENA Auto)
          ) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  G  :  Groupoid
2.  x00  :  cat-ob(cat(G))
3.  x10  :  cat-ob(cat(G))
4.  x01  :  cat-ob(cat(G))
5.  x11  :  cat-ob(cat(G))
6.  a  :  cat-arrow(cat(G))  x00  x10
7.  b  :  cat-arrow(cat(G))  x10  x11
8.  c  :  cat-arrow(cat(G))  x00  x01
\mvdash{}  a  o  b  =  c  o  cat-comp(cat(G))  x01  x10  x11 
                            (cat-comp(cat(G))  x01  x00  x10  groupoid-inv(G;x00;x01;c)  a) 
                            b


By

---

Latex:
TACTIC:(Unfold  `cat-square-commutes`  0
                THEN  (RWW  "cat-comp-assoc<  groupoid-right-cancellation  groupoid\_inv.1  cat-comp-ident.1"  0\mcdot{}
                            THENA  Auto
                            )
                )

---

Home Index