---

Step * of Lemma cubical-sigma-fun_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[B,B':{G.A ⊢ _}]. ∀[f:{G.A ⊢ _:(B ⟶ B')}].
  (cubical-sigma-fun(G;A;B;f) ∈ {G ⊢ _:(Σ A B ⟶ Σ A B')})
BY
{ PresheafMLTTInstance Obid: presheaf-sigma-fun_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[B,B':\{G.A  \mvdash{}  \_\}].  \mforall{}[f:\{G.A  \mvdash{}  \_:(B  {}\mrightarrow{}  B')\}].
    (cubical-sigma-fun(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:(\mSigma{}  A  B  {}\mrightarrow{}  \mSigma{}  A  B')\})


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-sigma-fun\_wf\mcdot{}

---

Home Index