---

Step * of Lemma cc-adjoin-cube_wf

No Annotations
∀X:j⊢. ∀A:{X ⊢ _}. ∀J:fset(ℕ). ∀v:X(J). ∀u:A(v).  ((v;u) ∈ X.A(J))
BY
{ PresheafMLTTInstance Obid: psc-adjoin-set_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}J:fset(\mBbbN{}).  \mforall{}v:X(J).  \mforall{}u:A(v).    ((v;u)  \mmember{}  X.A(J))


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-adjoin-set\_wf\mcdot{}

---

Home Index