---

Step * of Lemma pscm-ap-presheaf-app

No Annotations
∀[C:SmallCategory]. ∀[X,Delta:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[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)[u])s})
BY
{ (Intros
   THEN (RWO  "pscm-presheaf-app<" 0 THENA Auto)
   THEN Fold `member` 0
   THEN InstLemma `presheaf-app_wf` [⌜C⌝;⌜X⌝;⌜A⌝;⌜B⌝;⌜w⌝;⌜u⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Delta:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:\mPi{}A  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:
(Intros
  THEN  (RWO    "pscm-presheaf-app<"  0  THENA  Auto)
  THEN  Fold  `member`  0
  THEN  InstLemma  `presheaf-app\_wf`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index