---

Step * of Lemma presheaf-lam_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[b:{X.A ⊢ _:(B)p}].
  (presheaf-lam(X;b) ∈ {X ⊢ _:(A ⟶ B)})
BY
{ (Intros
   THEN (InstLemma `presheaf-fun-as-presheaf-pi` [⌜C⌝;⌜X⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (Assert presheaf-lam(X;b) ∈ {X ⊢ _:ΠA (B)p} BY
               ProveWfLemma)
   THEN InferEqualType
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[b:\{X.A  \mvdash{}  \_:(B)p\}].
    (presheaf-lam(X;b)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\})


By

---

Latex:
(Intros
  THEN  (InstLemma  `presheaf-fun-as-presheaf-pi`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  presheaf-lam(X;b)  \mmember{}  \{X  \mvdash{}  \_:\mPi{}A  (B)p\}  BY
                          ProveWfLemma)
  THEN  InferEqualType
  THEN  Auto)

---

Home Index