Step
*
of Lemma
cubical-pi-intro
No Annotations
∀G:j⊢. ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}. ({G.A ⊢ _:B}
⇒ {G ⊢ _:ΠA 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