---

Step * of Lemma csm-cubical-sigma

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

---

Latex:

---

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


By

---

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

---

Home Index