---

Step * of Lemma cubical-type-rev-iso_wf

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

---

Latex:

---

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


By

---

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

---

Home Index