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?