---

Step * of Lemma functor-arrow_wf

∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].
  (functor-arrow(F) ∈ x:cat-ob(C)
   ⟶ y:cat-ob(C)
   ⟶ (cat-arrow(C) x y)
   ⟶ (cat-arrow(D) (functor-ob(F) x) (functor-ob(F) y)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].
    (functor-arrow(F)  \mmember{}  x:cat-ob(C)
      {}\mrightarrow{}  y:cat-ob(C)
      {}\mrightarrow{}  (cat-arrow(C)  x  y)
      {}\mrightarrow{}  (cat-arrow(D)  (functor-ob(F)  x)  (functor-ob(F)  y)))


By

---

Latex:
ProveWfLemma

---

Home Index