Step
*
of Lemma
csm-cubical-pi
No Annotations
∀X,Delta:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta j⟶ X.  ((ΠA B)s = Delta ⊢ Π(A)s (B)(s o 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