The Interval type in Hott vs. in real analysis

The Interval type in Hott vs. in real analysis

[du yu]

[-- Attachment #1.1: Type: text/plain, Size: 294 bytes --]

I have seen the definition of Interval type [0,1] in HoTT book as higher 
inductive type and in cubical type theory as De-morgan algebra, and in real 
analysis there exists continuous function from [0,1] to Real,which means 
[0,1] is equivalent to R . How are these thing relate to each other?

[-- Attachment #1.2: Type: text/html, Size: 311 bytes --]

Re: [HoTT] The Interval type in Hott vs. in real analysis

[Michael Shulman]

The higher inductive "homotopical" interval is a very different thing
from the "topological" interval of real numbers.  The connection is
that the homotopical interval is the "shape" or "fundamental
infinity-groupoid" of the topological interval.  The tradition in
homotopy theory of identifying topological spaces with their shapes,
or differently-put of studying infinity-groupoids indirectly by way of
topological spaces whose shapes they are, leads to the confusion and
the coincidence of names.

On Tue, Oct 17, 2017 at 9:39 AM, du yu <doof...@gmail.com> wrote:
> I have seen the definition of Interval type [0,1] in HoTT book as higher
> inductive type and in cubical type theory as De-morgan algebra, and in real
> analysis there exists continuous function from [0,1] to Real,which means
> [0,1] is equivalent to R . How are these thing relate to each other?
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.