---

Step * of Lemma cubical-type-iso-inverse

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  ((cubical-type-rev-iso(X)  o  cubical-type-iso(X))  =  (\mlambda{}x.x))


By

---

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

---

Home Index