Jason Gross (Feb 15 2022 at 21:55): 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 ?)
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.paradoxwhereNProp := { 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.
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.)
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.
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).
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: Sep 30 2023 at 05:01 UTC