Martin Escardo on Nostr: In summary, we have: (1) If 𝓤 is univalent *and* funext 𝓤 𝓤⁺ holds, then ...

In summary, we have:

(1) If 𝓤 is univalent *and* funext 𝓤 𝓤⁺ holds, then the map χ is an equivalence.

(2) If χ is an equivalence *and* funext 𝓤 𝓤⁺ and propext 𝓤 both hold, then 𝓤 is univalent (and hence propext 𝓤 holds).

So we almost have that 𝓤 is univalent if and only if χ is an equivalence, but not quite.

In one direction we additionally need funext 𝓤 𝓤⁺, and in the other direction we additionally need propext 𝓤 (which is a particular case of the univalence of 𝓤).

This is kind of annoying.

Can we get rid of the additional hypotheses?

Ideally, we would like to have that 𝓤 is univalent if and only if the map χ is an equivalence.

In any case this TypeTopology file proves the above (and more):

https://martinescardo.github.io/TypeTopology/UF.Classifiers.html

5/5