---

Step * of Lemma cubical-type-iso_wf

No Annotations
∀[X:j⊢]. (cubical-type-iso(X) ∈ cubical_type{i:l}(X) ⟶ {X ⊢' _})
BY
{ PresheafMLTTInstance Obid: presheaf-type-iso_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  (cubical-type-iso(X)  \mmember{}  cubical\_type\{i:l\}(X)  {}\mrightarrow{}  \{X  \mvdash{}'  \_\})


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-type-iso\_wf\mcdot{}

---

Home Index