## Stream: Coq users

### Topic: Hurkens on decidable subfinite propositions?

#### 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.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.

#### 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