---

Step * of Lemma cubical-type-sq-presheaf-type

∀[X:Top]. ({X ⊢ _} ~ {X ⊢ _})
BY
{ (Auto THEN PresheafUnfolding) }

---

Latex:

---

Latex:
\mforall{}[X:Top].  (\{X  \mvdash{}  \_\}  \msim{}  \{X  \mvdash{}  \_\})


By

---

Latex:
(Auto  THEN  PresheafUnfolding)

---

Home Index