---

Step * of Lemma csm-cubical-fun-family

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

---

Latex:

---

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


By

---

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

---

Home Index