Naïm Camille Favier on Nostr: nprofile1q…chszg I don't think you can: this seems to require at least ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4sqchszg (nprofile…hszg) I don't think you can: this seems to require at least (-2)-univalence ("all contractible types in 𝓤 are equal") (see also this answer by nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq3p50dwg48ec85vc22dr2u3xj5knm5jpn0p8kvvffcxvxl2djkgqqwd2pts (nprofile…2pts) ; I don't know if either of you inspired the other).

As a counterexample, consider the Tarski universe with two distinct unit types and nothing else, 𝓤 = (2, λ _ → ⊤). This is clearly not univalent, nor even (-2)-univalent, but it can be closed under Σ and Id in such a way that χ and τ are fibrewise inverses (where τ is the map assigning total spaces to functions into 𝓤).

To see this, note that closing 𝓤 under Σ amounts to choosing a function σ : 2 × 2 → 2, while closing 𝓤 under Id amounts to choosing a function ι : 2 → 2. Then, under the obvious identifications (⊤ → 2) = ((X : 2) × ⊤ → ⊤) = 2, we have

χ Y X = σ X (ι Y)
τ Y X = σ Y X

Thus the two maps can be made into fibrewise inverses of each other by choosing ι to be the identity and σ to be XOR.

The question in your first post is even easier to refute, as it doesn't ask that χ or τ be a fibrewise equivalence; only that there is some fibrewise equivalence. We can even find a counterexample that satisfies (-1)-univalence: take 𝓤 = (ℕ, Fin). This is not univalent (because it is a set and contains the booleans), but it is (-1)-univalent, and the domain and codomain of χ Y are both countably infinite when Y > 0 and equal to 1 when Y = 0, so they are fibrewise equivalent.

Of course, χ can't be a fibrewise equivalence since that would imply that ℕ is univalent; the cardinality of the fibre of χ Y at a function f : Fin Y → ℕ seems to be the multinomial coefficient of f.

(nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqg7p0zthkpmec86usnemp047qh2gcmlp364hslxtmwcd5hfhjpewsx3ujms (nprofile…ujms) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpql4satj4aqvl92cvn9eatefl25n9g3vm8y5skgftkrwpczg0jj98qpl4vq9 (nprofile…4vq9) can you check that I'm not bullshitting too much?)