---

Step * of Lemma pscm-ap-presheaf-app-fun

No Annotations
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[w:{X ⊢ _:(A ⟶ B)}]. ∀[u:{X ⊢ _:A}].
∀[s:psc_map{j:l}(C; Delta; X)].
  ((app(w; u))s = app((w)s; (u)s) ∈ {Delta ⊢ _:(B)s})
BY
{ (Auto
   THEN (InstLemma `presheaf-fun-as-presheaf-pi` [⌜X⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstLemma `pscm-ap-presheaf-app` [⌜X⌝;⌜Delta⌝;⌜A⌝;⌜(B)p⌝;⌜w⌝;⌜u⌝;⌜s⌝]⋅ THENA Auto)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Delta:ps\_context\{j:l\}(C)].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}].
\mforall{}[u:\{X  \mvdash{}  \_:A\}].  \mforall{}[s:psc\_map\{j:l\}(C;  Delta;  X)].
    ((app(w;  u))s  =  app((w)s;  (u)s))


By

---

Latex:
(Auto
  THEN  (InstLemma  `presheaf-fun-as-presheaf-pi`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `pscm-ap-presheaf-app`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index