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 ?)

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.

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

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

for some `n`

.

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`

).

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