The Coq mailing list

[Steven Schäfer <s.schaefer89 AT googlemail.com>]

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!