---

Step * of Lemma op-functor_wf

∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (op-functor(F) ∈ Functor(op-cat(C);op-cat(D)))
BY
{ (Auto
   THEN Unfold `op-functor` 0
   THEN (MemCD THENW Auto)
   THEN RWW "cat_ob_op_lemma op-cat-arrow op-cat-comp op-cat-id" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].    (op-functor(F)  \mmember{}  Functor(op-cat(C);op-cat(D)))


By

---

Latex:
(Auto
  THEN  Unfold  `op-functor`  0
  THEN  (MemCD  THENW  Auto)
  THEN  RWW  "cat\_ob\_op\_lemma  op-cat-arrow  op-cat-comp  op-cat-id"  0
  THEN  Auto)

---

Home Index