From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Tue, 17 Oct 2017 09:39:37 -0700 (PDT)
From: du yu <doof...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <bc6ceb84-9d61-4c35-9179-d688803fd110@googlegroups.com>
Subject: The Interval type in Hott vs. in real analysis
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_21057_408762199.1508258377987"

------=_Part_21057_408762199.1508258377987
Content-Type: multipart/alternative; 
	boundary="----=_Part_21058_98293831.1508258377987"

------=_Part_21058_98293831.1508258377987
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

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?

------=_Part_21058_98293831.1508258377987
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: 7bit

<div dir="ltr">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?</div>
------=_Part_21058_98293831.1508258377987--

------=_Part_21057_408762199.1508258377987--