---

Step * of Lemma op-cat-comp

∀C:SmallCategory. ∀[I,J,K,f,g:Top].  (cat-comp(op-cat(C)) I J K f g ~ cat-comp(C) K J I g f)
BY
{ ((UnivCD THENA Auto) THEN DCat 1 THEN RepUR ``op-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}[I,J,K,f,g:Top].    (cat-comp(op-cat(C))  I  J  K  f  g  \msim{}  cat-comp(C)  K  J  I  g  f)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  DCat  1  THEN  RepUR  ``op-cat``  0  THEN  Auto)

---

Home Index