---

Step * 2 of Lemma groupoid-square-commutes-iff2


1. G : Groupoid
2. x : cat-ob(cat(G))
3. y1 : cat-ob(cat(G))
4. y2 : cat-ob(cat(G))
5. z : cat-ob(cat(G))
6. x_y1 : cat-arrow(cat(G)) x y1
7. y1_z : cat-arrow(cat(G)) y1 z
8. x_y2 : cat-arrow(cat(G)) x y2
9. y2_z : cat-arrow(cat(G)) y2 z
10. x_y1
= (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y2 z x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
∈ (cat-arrow(cat(G)) x y1)
⊢ (cat-comp(cat(G)) x y1 z x_y1 y1_z) = (cat-comp(cat(G)) x y2 z x_y2 y2_z) ∈ (cat-arrow(cat(G)) x z)
BY
{ ((HypSubst' (-1) 0 THENA Auto) THEN (RWO  "cat-comp-assoc" 0 THENA Auto) THEN RWO "groupoid_inv.2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  x  :  cat-ob(cat(G))
3.  y1  :  cat-ob(cat(G))
4.  y2  :  cat-ob(cat(G))
5.  z  :  cat-ob(cat(G))
6.  x$_{y1}$  :  cat-arrow(cat(G))  x  y1
7.  y1$_{z}$  :  cat-arrow(cat(G))  y1  z
8.  x$_{y2}$  :  cat-arrow(cat(G))  x  y2
9.  y2$_{z}$  :  cat-arrow(cat(G))  y2  z
10.  x$_{y1}$  =  (cat-comp(cat(G))  x  z  y1  (cat-comp(cat(G))  x  y2  z  x$_\mbackslash{}ff7\000Cby2}$  y2$_{z}$)  groupoid-inv(G;y1;z;y1$_{z}$))
\mvdash{}  (cat-comp(cat(G))  x  y1  z  x$_{y1}$  y1$_{z}$)  =  (cat-comp(ca\000Ct(G))  x  y2  z  x$_{y2}$  y2$_{z}$)


By

---

Latex:
((HypSubst'  (-1)  0  THENA  Auto)
  THEN  (RWO    "cat-comp-assoc"  0  THENA  Auto)
  THEN  RWO  "groupoid\_inv.2"  0
  THEN  Auto)

---

Home Index