Discussion:
[Coq-Club] coq + higher inductive types + proof irrelevance?
Abhishek Anand
2018-07-26 21:27:33 UTC
Permalink
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/
Jason -Zhong Sheng- Hu
2018-07-27 01:02:52 UTC
Permalink
Can I read the question as asking if axiom K/UIP consistent with CIC? Or are you asking if `forall (P Q : Prop), (P <-> Q) <-> (P = Q)` is consistent with CIC?


- Jason

________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Abhishek Anand <***@gmail.com>
Sent: July 26, 2018 5:27:33 PM
To: coq-club
Subject: [Coq-Club] coq + higher inductive types + proof irrelevance?

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/
Steven Schäfer
2018-07-27 07:32:40 UTC
Permalink
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
Post by Abhishek Anand
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/
Bas Spitters
2018-07-27 07:49:58 UTC
Permalink
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
Post by Steven Schäfer
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
Post by Abhishek Anand
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/
Siddharth Bhat
2018-07-27 07:57:12 UTC
Permalink
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
Post by Bas Spitters
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
Post by Steven Schäfer
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
Post by Abhishek Anand
I understand that UIP (implied by proof irrelevance) is inconsistent
with
Post by Steven Schäfer
Post by Abhishek Anand
univalence.
Can higher inductive types (or just some kind of "level 1" quotients
where I
Post by Steven Schäfer
Post by Abhishek Anand
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!
Steven Schäfer
2018-07-27 09:39:37 UTC
Permalink
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
Post by Siddharth Bhat
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
Post by Bas Spitters
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
Post by Steven Schäfer
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
Post by Abhishek Anand
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!
Bas Spitters
2018-07-27 10:40:28 UTC
Permalink
Correct, that's the way Vladimir did it in Foundations.

On Fri, Jul 27, 2018 at 11:39 AM, Steven Schäfer
Post by Steven Schäfer
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
Post by Siddharth Bhat
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
Post by Bas Spitters
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
Post by Steven Schäfer
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
Post by Abhishek Anand
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!
Abhishek Anand
2018-10-17 22:02:23 UTC
Permalink
Post by Steven Schäfer
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.
I do want computation rules on paths (I mean inductive constructors of
equality). I don't understand how computation on paths violates UIP in the
absence of univalence.
Is there an easy construction demonstrating the problem without needing to
understand scary-sounding concepts such as homotopy pushouts.
Post by Steven Schäfer
- Steven
Post by Abhishek Anand
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
Post by Abhishek Anand
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/
--
-- Abhishek
http://www.cs.cornell.edu/~aa755/
Steven Schäfer
2018-10-18 09:38:54 UTC
Permalink
I don't remember what I had in mind, but I'm almost sure that it was wrong.

For example, in the presence of UIP, the unit type satisfies the induction
principle for the circle (trivially, since "base = base" is equivalent to
"unit"). So in fact, the opposite should be true: in the presence of UIP,
the path computation rules hold vacuously, since paths are proof
irrelevant...

Am Do., 18. Okt. 2018 um 00:03 Uhr schrieb Abhishek Anand <
Post by Abhishek Anand
Post by Steven Schäfer
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.
I do want computation rules on paths (I mean inductive constructors of
equality). I don't understand how computation on paths violates UIP in the
absence of univalence.
Is there an easy construction demonstrating the problem without needing to
understand scary-sounding concepts such as homotopy pushouts.
Post by Steven Schäfer
- Steven
Post by Abhishek Anand
I understand that UIP (implied by proof irrelevance) is inconsistent
with
Post by Abhishek Anand
univalence.
Can higher inductive types (or just some kind of "level 1" quotients
where I
Post by Abhishek Anand
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/
--
-- Abhishek
http://www.cs.cornell.edu/~aa755/
Loading...