From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 20 Mar 2017 08:12:40 -0700 (PDT)
From: Matt Oliveri <atm...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Cc: univalent-...@googlegroups.com, vlad...@ias.edu
Message-Id: <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com>
In-Reply-To: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu>
References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu>
Subject: Re: about the HTS
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_984_752956129.1490022760922"

------=_Part_984_752956129.1490022760922
Content-Type: multipart/alternative; 
	boundary="----=_Part_985_159958803.1490022760922"

------=_Part_985_159958803.1490022760922
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

So the answer was yes, right? Problem solved?

On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
>
> Just a thought=E2=80=A6 Can we devise a version of the HTS where exact eq=
uality=20
> types are not available for the universes such that, even with the exact=
=20
> equality, HTS would remain a univalent theory.=20
>
> Maybe only some types should be equipped with the exact equality and this=
=20
> should be a special quality of types.=20
>
> Vladimir.=20
>
> PS If there are higher inductive types then the exact equality should not=
=20
> be available for them either.
>

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

<div dir=3D"ltr">So the answer was yes, right? Problem solved?<br><br>On Th=
ursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:<blockquote class=
=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;border-left: 1px #cc=
c solid;padding-left: 1ex;">Just a thought=E2=80=A6 Can we devise a version=
 of the HTS where exact equality types are not available for the universes =
such that, even with the exact equality, HTS would remain a univalent theor=
y.
<br>
<br>Maybe only some types should be equipped with the exact equality and th=
is should be a special quality of types.
<br>
<br>Vladimir.
<br>
<br>PS If there are higher inductive types then the exact equality should n=
ot be available for them either.<br></blockquote></div>
------=_Part_985_159958803.1490022760922--

------=_Part_984_752956129.1490022760922--