---

Step * of Lemma cat-square-commutes-comp

∀[C:SmallCategory]. ∀[x1,x2,x3,y1,y2,y3:cat-ob(C)]. ∀[x1_y1:cat-arrow(C) x1 y1]. ∀[x2_y2:cat-arrow(C) x2 y2].
∀[x3_y3:cat-arrow(C) x3 y3]. ∀[y1_y2:cat-arrow(C) y1 y2]. ∀[y2_y3:cat-arrow(C) y2 y3]. ∀[x1_x2:cat-arrow(C) x1 x2].
∀[x2_x3:cat-arrow(C) x2 x3].
  (x1_y1 o cat-comp(C) y1 y2 y3 y1_y2 y2_y3 = cat-comp(C) x1 x2 x3 x1_x2 x2_x3 o x3_y3) supposing 
     (x1_y1 o y1_y2 = x1_x2 o x2_y2 and 
     x2_y2 o y2_y3 = x2_x3 o x3_y3)
BY
{ (Auto
   THEN All (Unfold `cat-square-commutes`)
   THEN (RW CatNormC 0 THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "cat-comp-assoc" 0 THENA Auto)
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[x1,x2,x3,y1,y2,y3:cat-ob(C)].  \mforall{}[x1$_{y1}$:cat-arrow(C)  x1  \000Cy1].  \mforall{}[x2$_{y2}$:cat-arrow(C) 
                                                                                                                                                                              x2 
                                                                                                                                                                              y2].
\mforall{}[x3$_{y3}$:cat-arrow(C)  x3  y3].  \mforall{}[y1$_{y2}$:cat-arrow(C)  y1\000C  y2].  \mforall{}[y2$_{y3}$:cat-arrow(C)  y2  y3].
\mforall{}[x1$_{x2}$:cat-arrow(C)  x1  x2].  \mforall{}[x2$_{x3}$:cat-arrow(C)  x2\000C  x3].
    (x1$_{y1}$  o  cat-comp(C)  y1  y2  y3  y1$_{y2}$  y2$_\mbackslash{}f\000Cf7by3}$  =  cat-comp(C)  x1  x2  x3  x1$_{x2}$  x2$_{x3}$  o\000C  x3$_{y3}$)  supposing 
          (x1$_{y1}$  o  y1$_{y2}$  =  x1$_{x2}$  \000Co  x2$_{y2}$  and 
          x2$_{y2}$  o  y2$_{y3}$  =  x2$_{x3}$  o\000C  x3$_{y3}$)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `cat-square-commutes`)
  THEN  (RW  CatNormC  0  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "cat-comp-assoc"  0  THENA  Auto)
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index