The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

Could you please expand on "propositional truncation" and what that means?

I googled, and what I gather is that it is some existential witness of inhabitation of a type that does not provide an explicit witness?

If so, I don't see how this gives rise to quotients -- could you please give me a sketch of the construction? 

Thanks,

siddharth

On Fri 27 Jul, 2018, 13:20 Bas Spitters, <b.a.w.spitters AT gmail.com> wrote:

Matthieu and Amin recently went through such questions in the set model of CIC:
drops.dagstuhl.de/opus/volltexte/2018/9199/pdf/LIPIcs-FSCD-2018-29.pdf

On Fri, Jul 27, 2018 at 9:32 AM, Steven Schäfer
<s.schaefer89 AT googlemail.com> wrote:
> Hi Abhishek,
>
> Quotient types exist and proof irrelevance (along with propositional
> and functional extensionality) holds in the setoid model of type
> theory. The difference to higher-inductive types is that you cannot
> add computation rules on paths, since that would give you homotopy
> pushouts and thus also the circle and other non-hsets.
>
> If you are worried about consistency you could also just axiomatize
> the "propositional trunctation" (or rather, squash types as in NuPRL)
> and then derive quotient types from that together with funext/propext.
>
> - Steven
>
> 2018-07-26 23:27 GMT+02:00 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:
>> I understand that UIP (implied by proof irrelevance) is inconsistent with
>> univalence.
>>
>> Can higher inductive types (or just some kind of "level 1" quotients where I
>> don't care about distinguishing equality proofs) be added to Coq without
>> needing to blacklist the proof irrelevance axiom?
>>
>> --
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/

--

Sending this from my phone, please excuse any typos!