---

Step * of Lemma cubical-type-iso-inverse2

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

---

Latex:

---

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


By

---

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

---

Home Index