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 | View the thread | More toots from andrejbauer@mathstodon.xyz
text/geminiThis content has been proxied by September (ba2dc).