The Coq mailing list

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

Correct, that's the way Vladimir did it in Foundations.

On Fri, Jul 27, 2018 at 11:39 AM, Steven Schäfer
<s.schaefer89 AT googlemail.com>
 wrote:
> The propositional truncation of a type "A" is a type "trunc A" with a
> constructor "tr : A -> trunc A" and an elimination principle into all
> h-propositions (singleton types) "trec : forall B, (forall x y : B, x
> = y) -> (A -> B) -> trunc A -> B" with the appropriate beta reduction
> rule "trec B H f (tr x) = f x".
>
> From this, together with functional and propositional extensionality,
> you can build quotients in the same way as you usually do it in set
> theory, as the type of inhabited equivalence classes of an equivalence
> relation. The trick is that that the existential quantifier is built
> from the propositional truncation of a dependent sum, instead of using
> the existential quantifier in Prop.
>
> For example, let "R : A -> A -> Prop" be an equivalence relation. Then
> the quotient of A by R can be defined as
>
> Definition quot := { P : A -> Prop & trunc { x : A | P = R x } }.
>
> I think I've seen this in the unimath library, but I'm not sure.
>
> - Steven
>
> 2018-07-27 9:57 GMT+02:00 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!