Step * of Lemma cubical-pi-intro

No Annotations
G:j⊢. ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}.  ({G.A ⊢ _:B}  {G ⊢ _:ΠB})
BY
PresheafMLTTInstance Obid: presheaf-pi-intro⋅ }


Latex:


Latex:
No  Annotations
\mforall{}G:j\mvdash{}.  \mforall{}A:\{G  \mvdash{}  \_\}.  \mforall{}B:\{G.A  \mvdash{}  \_\}.    (\{G.A  \mvdash{}  \_:B\}  {}\mRightarrow{}  \{G  \mvdash{}  \_:\mPi{}A  B\})


By


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




Home Index