---

Step * of Lemma functor-presheaf_wf

∀[C,D:SmallCategory].  ∀F:Functor(C;D). ∀P:Presheaf(D).  (functor-presheaf(F;P) ∈ Presheaf(C))
BY
{ (Auto THEN All (Unfold `presheaf`) THEN Unfold `functor-presheaf` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  All  (Unfold  `presheaf`)  THEN  Unfold  `functor-presheaf`  0  THEN  Auto)

---

Home Index