Step * of Lemma csm-cubical-pi

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


Latex:


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


By


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




Home Index