---

Step * of Lemma discrete-cube_wf

No Annotations
∀[A:𝕌{j}]. discrete-cube(A) j⊢
BY
{ PresheafMLTTInstance Obid: discrete-set_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:\mBbbU{}\{j\}].  discrete-cube(A)  j\mvdash{}


By

---

Latex:
PresheafMLTTInstance  Obid:  discrete-set\_wf\mcdot{}

---

Home Index