From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 1 Jun 2018 14:27:24 -0700 (PDT)
From: Matt Oliveri <atm...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <864df164-59e9-4609-8e81-7c334be11e98@googlegroups.com>
In-Reply-To: <CAGYJgtaFm3OTCWBbeyZrrpVdqYH7GbFbyTT7O9t0gEhSfW5fpg@mail.gmail.com>
References: <CAOvivQxmrTLRW8wk7cu+A9zF3LCrXSfqsp6R2UN_sz9tF-5UHQ@mail.gmail.com>
 <CAOvivQyY1k+KE9PztsNq6uhZGuV9D3pOYznnbB4p81s4=iHK0g@mail.gmail.com>
 <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk>
 <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8vK6FwQSkGg@mail.gmail.com>
 <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk>
 <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk>
 <CAOvivQzSuvhvvhLs0jR2ADTPUR9cKG2NucADJqe=Oer_EB0aaQ@mail.gmail.com>
 <D040F1EA-B812-4703-87CD-840E80DBE5CA@exmail.nottingham.ac.uk>
 <CAOvivQzU1M1gh63RxegZWuzw2LT2b-vsUuSEiB49LAOgJouW6Q@mail.gmail.com>
 <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com>
 <CAGYJgtaFm3OTCWBbeyZrrpVdqYH7GbFbyTT7O9t0gEhSfW5fpg@mail.gmail.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_10891_96265151.1527888444236"

------=_Part_10891_96265151.1527888444236
Content-Type: multipart/alternative; 
	boundary="----=_Part_10892_2084848911.1527888444236"

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

On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote:
>
> So from an internal perspective, I cannot think of any reason to
> insist on decidability.
>

I agree with this. And in particular, I think QIITs can define intrinsic 
syntax of (fully-annotated) extensional type theroy just fine. Equality 
reflection would be an extra equality constructor. Isn't that right? What 
do Thorsten and team think of that? Is it an infelicity of QIITs, perhaps 
because they're hSet truncated? Or is there a problem with ETT that 
structuralism doesn't shed light on? Or is ETT maybe not so bad?

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

<div dir="ltr">On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr">So from an internal perspective, I cannot think of any reason to<div style="font-size:13px">insist on decidability.</div></div></blockquote><div><br>I agree with this. And in particular, I think QIITs can define intrinsic syntax of (fully-annotated) extensional type theroy just fine. Equality reflection would be an extra equality constructor. Isn&#39;t that right? What do Thorsten and team think of that? Is it an infelicity of QIITs, perhaps because they&#39;re hSet truncated? Or is there a problem with ETT that structuralism doesn&#39;t shed light on? Or is ETT maybe not so bad?<br></div></div>
------=_Part_10892_2084848911.1527888444236--

------=_Part_10891_96265151.1527888444236--