---

Step * of Lemma discrete-map-is-constant

No Annotations
∀[T:𝕌{j}]. ∀[I:fset(ℕ)]. ∀[s:formal-cube(I) ij⟶ discrete-cube(T)].
  (s = (λJ,g. (s I 1)) ∈ formal-cube(I) ij⟶ discrete-cube(T))
BY
{ PresheafMLTTInstance Obid: ps-discrete-map-is-constant⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}\{j\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[s:formal-cube(I)  ij{}\mrightarrow{}  discrete-cube(T)].    (s  =  (\mlambda{}J,g.  (s  I  1)))


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-discrete-map-is-constant\mcdot{}

---

Home Index