From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 18 Dec 2017 04:09:31 -0800 (PST)
From: Matt Oliveri <atm...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <58e6faf9-7b23-44ae-a039-ef17f770cd2e@googlegroups.com>
In-Reply-To: <A88995F3-43D1-43A2-A448-3C6EFC422D8E@exmail.nottingham.ac.uk>
References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com>
 <BB338612-ECF6-42F8-B672-6276F5D7BCE8@exmail.nottingham.ac.uk>
 <CAOSJkmwoF3pFLw+YpqS5QKE3eNbOf2v2TyURsVx9AGK-RwygZg@mail.gmail.com>
 <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk>
 <20171212120233.GA32661@mathematik.tu-darmstadt.de>
 <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk>
 <20171215170011.GA22027@mathematik.tu-darmstadt.de>
 <D65BDF23.A4EFB%psztxa@exmail.nottingham.ac.uk>
 <20171217102151.GA16619@mathematik.tu-darmstadt.de>
 <D65C0347.A4F0B%psztxa@exmail.nottingham.ac.uk>
 <f4747ed9-fc19-453b-ad2e-f94f06e4e091@googlegroups.com>
 <A88995F3-43D1-43A2-A448-3C6EFC422D8E@exmail.nottingham.ac.uk>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof
 irrelevance consistent?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_3156_1995547305.1513598971584"

------=_Part_3156_1995547305.1513598971584
Content-Type: multipart/alternative; 
	boundary="----=_Part_3157_855885117.1513598971584"

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

I don't understand these things you wrote:

On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote:
>
> Interestingly it seems that QITs are more expressive then quotients (which 
> can be encoded impredicatively).
>
>
> And as I said above, QITs are an interesting extension which in some 
> instances avoids appealing to the axiom of choice.
>

Like, in a constructive, predicative system without any choice principles, 
and where quotients are not expressed as QITs, is there an expressiveness 
difference? (I'm thinking of Computational Type Theory, for example.)

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

<div dir="ltr">I don&#39;t understand these things you wrote:<br><br>On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">







<div bgcolor="white" link="blue" vlink="purple" lang="EN-GB">
<div>Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively).<div>
<p class="MsoNormal"><br>And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice.</p></div></div></div></blockquote><div><br>Like, in a constructive, predicative system without any choice principles, and where quotients are not expressed as QITs, is there an expressiveness difference? (I&#39;m thinking of Computational Type Theory, for example.)<br></div></div>
------=_Part_3157_855885117.1513598971584--

------=_Part_3156_1995547305.1513598971584--