Step * of Lemma discrete-cubical-term-is-constant

[T:Type]. ∀[I:fset(ℕ)]. ∀[t:{formal-cube(I) ⊢ _:discr(T)}].  (t discr(t(1)) ∈ {formal-cube(I) ⊢ _:discr(T)})
BY
PresheafMLTTInstance Obid: discrete-presheaf-term-is-constant⋅ }


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[t:\{formal-cube(I)  \mvdash{}  \_:discr(T)\}].    (t  =  discr(t(1)))


By


Latex:
PresheafMLTTInstance  Obid:  discrete-presheaf-term-is-constant\mcdot{}




Home Index