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