---

Step * 1 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. (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)
⊢ 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)
BY
{ (RevHypSubst'  (-1) 0 THENA Auto) }

1
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. (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)
⊢ x_y1
= (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y1 z x_y1 y1_z) groupoid-inv(G;y1;z;y1_z))
∈ (cat-arrow(cat(G)) x y1)

---

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.  (cat-comp(cat(G))  x  y1  z  x$_{y1}$  y1$_{z}$)  =  (cat-comp(\000Ccat(G))  x  y2  z  x$_{y2}$  y2$_{z}$)
\mvdash{}  x$_{y1}$  =  (cat-comp(cat(G))  x  z  y1  (cat-comp(cat(G))  x  y2  z  x$_{y\000C2}$  y2$_{z}$)  groupoid-inv(G;y1;z;y1$_{z}$))


By

---

Latex:
(RevHypSubst'    (-1)  0  THENA  Auto)

---

Home Index