---

Step * of Lemma pscm-presheaf-lam

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[b:{X.A ⊢ _:(B)p}]. ∀[H:ps_context{j:l}(C)].
∀[s:psc_map{j:l}(C; H; X)].
  ((presheaf-lam(X;b))s = presheaf-lam(H;(b)s+) ∈ {H ⊢ _:((A ⟶ B))s})
BY
{ (Intros
   THEN Unfold `presheaf-lam` 0
   THEN (InstLemma `pscm-presheaf-lambda` [⌜C⌝;⌜X⌝;⌜A⌝;⌜(B)p⌝;⌜b⌝;⌜H⌝;⌜s⌝]⋅ THENA Auto)
   THEN InferEqualType
   THEN EqCDA
   THEN (RWO  "pscm-presheaf-pi pscm-presheaf-fun" 0 THENA Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. b : {X.A ⊢ _:(B)p}
6. H : ps_context{j:l}(C)
7. s : psc_map{j:l}(C; H; X)
8. ((λb))s = (λ(b)s+) ∈ {H ⊢ _:(ΠA (B)p)s}
⊢ H ⊢ Π(A)s ((B)p)(s o p;q) = (H ⊢ (A)s ⟶ (B)s) ∈ presheaf-type{[j' | i]:l}(C; H)

---

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\}].
\mforall{}[H:ps\_context\{j:l\}(C)].  \mforall{}[s:psc\_map\{j:l\}(C;  H;  X)].
    ((presheaf-lam(X;b))s  =  presheaf-lam(H;(b)s+))


By

---

Latex:
(Intros
  THEN  Unfold  `presheaf-lam`  0
  THEN  (InstLemma  `pscm-presheaf-lambda`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InferEqualType
  THEN  EqCDA
  THEN  (RWO    "pscm-presheaf-pi  pscm-presheaf-fun"  0  THENA  Auto))

---

Home Index