---

Step * of Lemma csm-cubical-pi-family

No Annotations
∀X,Delta:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta j⟶ X. ∀I:fset(ℕ). ∀a:Delta(I).
  (cubical-pi-family(X;A;B;I;(s)a) = cubical-pi-family(Delta;(A)s;(B)(s o p;q);I;a) ∈ Type)
BY
{ PresheafMLTTInstance Obid: pscm-presheaf-pi-family⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}s:Delta  j{}\mrightarrow{}  X.  \mforall{}I:fset(\mBbbN{}).  \mforall{}a:Delta(I).
    (cubical-pi-family(X;A;B;I;(s)a)  =  cubical-pi-family(Delta;(A)s;(B)(s  o  p;q);I;a))


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-presheaf-pi-family\mcdot{}

---

Home Index