Ancestors

Toot

Written by Andrej Bauer on 2024-11-06 at 10:07

Discussing the existence property with a very smart master's student resulted in the following epiphany: existence property with parameters is the same thing as equating ∃ and Σ.

Allow me to explain. The usual existence property states that if a closed statement ∃ (y : B) . φ(y) has a proof, then there is a closed term t : B such that φ(t).

Let "existence property with parameters" be the principle: for any provable statement ∃ (y : B) . φ(x, y), where x : A indicates that parameters are allowed, there is a term t(x) : B such that φ(x, t(x)) has a proof.

Well, if this principle holds then we will be able to show that ∃ (y : B) . φ(y) and Σ (y : B) . φ(y) are equivalent (in an arbitrary context). Indeed, suppose p : ∃ (y : B) . φ(y). By the existence property with parameters there is a term t(p) : B and a proof u(p) : φ(t(p)). The map taking p to (t(p), u(p)) is going to be an equivalence from ∃ (y : B) . φ(y) to Σ (y : B) . φ(y).

(The above argument can be made parametric in B and φ if we let B be a variable ranging over a universe and φ a variable of type B → Prop.)

Probably I just rediscovered something that's already in the HoTT book or TypeTopology or somewhere. I'd be interested in knowing about it.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Descendants

Written by Jon Sterling on 2024-11-06 at 10:47

@andrejbauer I am not sure this actually equates Exists and Sigma. It just establishes “inter-inhabitability” at the meta-level. You could imagine a type theory with this property in which, nonetheless, Sigma is not valued in mere propositions (whereas Exists is, by definition).

=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz

Written by Andrej Bauer on 2024-11-06 at 11:18

@jonmsterling I was shooting for an equivalence in the case where the family is propositionally-valued only. Shouldn't it work in that case?

Hmm, I suppose there is no guarantee that the existence property won't muck about and mess with the witnesses. Good point.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz