---

Step * of Lemma sub-cubical-set-true

No Annotations
∀[X:j⊢]. X | I,rho.True ≡ X
BY
{ PresheafMLTTInstance Obid: sub-presheaf-set-true⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  X  |  I,rho.True  \mequiv{}  X


By

---

Latex:
PresheafMLTTInstance  Obid:  sub-presheaf-set-true\mcdot{}

---

Home Index