Stream: Coq users

Topic: Hurkens on decidable subfinite propositions?


view this post on Zulip Jason Gross (Feb 15 2022 at 21:55):

Is there a version of Hurken's paradox that applies to the universe of decidable subfinite propositions. That is, I want a variant of Coq.Loigic.Hurkens.NoRetractToNegativeProp.paradox where NProp := { P : Prop | (P \/ ~P) /\ (exists n, forall (f : Fin.t n -> P), exists n1 n2, n1 <> n2 /\ f n1 = f n2) }. (cc @Hugo Herbelin ?)

view this post on Zulip Hugo Herbelin (Feb 15 2022 at 22:02):

Jason Gross said:

Is there a version of Hurken's paradox that applies to the universe of decidable subfinite propositions. That is, I want a variant of Coq.Loigic.Hurkens.NoRetractToNegativeProp.paradox where NProp := { P : Prop | (P \/ ~P) /\ (exists n, forall (f : Fin.t n -> P), exists n1 n2, n1 <> n2 /\ f n1 = f n2) }. (cc Hugo Herbelin ?)

Naively, I would say no, with the intuition that Hurkens encapsulates a quantification over a big object in a small type. This big quantification has no reason to preserve subfiniteness a priori. You should ask a more expert than me.

view this post on Zulip Jason Gross (Feb 15 2022 at 22:03):

I thought NProp was the universe of big objects, though? (I'm suggesting that all big objects, including the universe of small objects, be subfinite and decidable.)

view this post on Zulip Jason Gross (Feb 15 2022 at 22:05):

Actually, I think I'm interested in all big objects being strictly finite, i.e., equivalent to Fin.t n for some n.

view this post on Zulip Jason Gross (Feb 15 2022 at 23:07):

If there is such a variant of Hurkens, then I think you can show that Univalence is inconsistent with impredicative Prop unless -indices-matter is set (AFAIK, this was previously only folklore). Roughly the idea is that, if we assume funext, FiniteProp has True and False and is closed under forall. If we assume univalence, FiniteProp also has bool = bool. Then we should be able to get a retract between FiniteProp and bool = bool (where bool = bool -> FiniteProp -> bool = bool is the identity and FiniteProp -> bool = bool -> FiniteProp collapses each FiniteProp to either True or False).

view this post on Zulip Jason Gross (Feb 15 2022 at 23:31):

I've made a note of this at https://github.com/HoTT/HoTT/issues/842#issuecomment-1040903235


Last updated: Jan 31 2023 at 13:02 UTC