---

Step * of Lemma groupoid-square-commutes-iff

∀[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) x y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
∀[x_y2:cat-arrow(cat(G)) x y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;y2_z
  = (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y1 z x_y1 y1_z))
  ∈ (cat-arrow(cat(G)) y2 z))
BY
{ (Auto THEN All (RepUR ``cat-square-commutes``) THEN (HypSubst' (-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)
⊢ y2_z
= (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y2 z x_y2 y2_z))
∈ (cat-arrow(cat(G)) y2 z)

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

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[x,y1,y2,z:cat-ob(cat(G))].  \mforall{}[x$_{y1}$:cat-arrow(cat(G))  x  y1].  \000C\mforall{}[y1$_{z}$:cat-arrow(cat(G)) 
                                                                                                                                                                  y1 
                                                                                                                                                                  z].
\mforall{}[x$_{y2}$:cat-arrow(cat(G))  x  y2].  \mforall{}[y2$_{z}$:cat-arrow(cat\000C(G))  y2  z].
    uiff(x$_{y1}$  o  y1$_{z}$  =  x$_{y2}$  o  \000Cy2$_{z}$;y2$_{z}$
    =  (cat-comp(cat(G))  y2  x  z  groupoid-inv(G;x;y2;x$_{y2}$)  (cat-comp(cat(G))  x  y\000C1  z  x$_{y1}$  y1$_{z}$)))


By

---

Latex:
(Auto  THEN  All  (RepUR  ``cat-square-commutes``)  THEN  (HypSubst'  (-1)  0  THENA  Auto))

---

Home Index