The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

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/