Nuprl Lemma : discrete-cubical-term-is-map

∀[T:Type]. ∀[X:j⊢]. {X ⊢ _:discr(T)} ≡ X ij⟶ discrete-cube(T)

Proof

Error : references

Latex:
\mforall{}[T:Type]. \mforall{}[X:j\mvdash{}]. \{X \mvdash{} \_:discr(T)\} \mequiv{} X ij{}\mrightarrow{} discrete-cube(T) Date html generated: 2020_05_21-AM-10_30_08 Last ObjectModification: 2020_04_04-AM-09_49_15 Theory : cubical!type!theory Home Index