---

Step * of Lemma csm-cubical-fun

No Annotations
∀X,Delta:j⊢. ∀A,B:{X ⊢ _}. ∀s:Delta j⟶ X.  (((A ⟶ B))s = (Delta ⊢ (A)s ⟶ (B)s) ∈ {Delta ⊢ _})
BY
{ PresheafMLTTInstance Obid: pscm-presheaf-fun⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}A,B:\{X  \mvdash{}  \_\}.  \mforall{}s:Delta  j{}\mrightarrow{}  X.    (((A  {}\mrightarrow{}  B))s  =  (Delta  \mvdash{}  (A)s  {}\mrightarrow{}  (B)s))


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-presheaf-fun\mcdot{}

---

Home Index