---

Step * of Lemma cat-square-commutes-sym

∀[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) x y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) x 
                                                                                                         y2].
∀[y2_z:cat-arrow(C) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;x_y2 o y2_z = x_y1 o y1_z)
BY
{ (Auto THEN ParallelLast) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[x,y1,y2,z:cat-ob(C)].  \mforall{}[x$_{y1}$:cat-arrow(C)  x  y1].  \mforall{}[y1\mbackslash{}\000Cff24_{z}$:cat-arrow(C)  y1  z].
\mforall{}[x$_{y2}$:cat-arrow(C)  x  y2].  \mforall{}[y2$_{z}$:cat-arrow(C)  y2  z]\000C.
    uiff(x$_{y1}$  o  y1$_{z}$  =  x$_{y2}$  o  \000Cy2$_{z}$;x$_{y2}$  o  y2$_{z}$  =  x$\mbackslash{}ff\000C5f{y1}$  o  y1$_{z}$)


By

---

Latex:
(Auto  THEN  ParallelLast)

---

Home Index