---

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  PresheafUnfolding)

---

Home Index