From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 3 Jun 2016 04:53:47 -0700 (PDT)
From: Andrew Polonsky <andrew....@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <deb61dfc-f1f3-48fc-b208-b94caca612d4@googlegroups.com>
In-Reply-To: <5750A527.4060705@cs.bham.ac.uk>
References: <5750A527.4060705@cs.bham.ac.uk>
Subject: Re: What is UF, what is HoTT and what is a univalent type theory?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1832_1055518960.1464954827775"

------=_Part_1832_1055518960.1464954827775
Content-Type: multipart/alternative; 
	boundary="----=_Part_1833_1855506920.1464954827775"

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


>
> Let me then come to the last of the three questions. What is UTT 
> (univalent type theory)? As I conceive it: 
>
>      It is any Martin-Lof type theory that is compatible with the idea 
>      that equality/equivalence, as rendered by the identity type, is, 
>      in general, structure rather than merely a property. 
>

I find this definition somewhat puzzling.  Cubicaltt is certainly 
compatible with the idea that equality is equivalence.  But its path type 
seems to be a very different concept compared to Martin-Lof identity type.

What is a Martin-Lof type theory anyway?  Are type systems based on untyped 
conversion (eg. Coq) Martin-Lof type theories?  Are type theories with a 
different notion of equality (eg. observational or cubical type theories) 
also Martin-Lof type theories?

Andrew

------=_Part_1833_1855506920.1464954827775
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Let me then c=
ome to the last of the three questions. What is UTT
<br>(univalent type theory)? As I conceive it:
<br>
<br>=C2=A0 =C2=A0 =C2=A0It is any Martin-Lof type theory that is compatible=
 with the idea
<br>=C2=A0 =C2=A0 =C2=A0that equality/equivalence, as rendered by the ident=
ity type, is,
<br>=C2=A0 =C2=A0 =C2=A0in general, structure rather than merely a property=
.
<br></blockquote><div><br></div><div>I find this definition somewhat puzzli=
ng. =C2=A0Cubicaltt is certainly compatible with the idea that equality is =
equivalence. =C2=A0But its path type seems to be a very different concept c=
ompared to Martin-Lof identity type.</div><div><br></div><div>What is a Mar=
tin-Lof type theory anyway? =C2=A0Are type systems based on untyped convers=
ion (eg. Coq) Martin-Lof type theories? =C2=A0Are type theories with a diff=
erent notion of equality (eg. observational or cubical type theories) also =
Martin-Lof type theories?</div><div><br></div><div>Andrew</div></div>
------=_Part_1833_1855506920.1464954827775--

------=_Part_1832_1055518960.1464954827775--