---

Step * of Lemma cubical-pi-implies-sigma

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

---

Latex:

---

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


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-pi-implies-sigma\mcdot{}

---

Home Index