Universe issues: relating across universes

Stream: Infinity-Cosmos

[Thomas Murrills]

I've been thinking about universe issues both in the specific case of SSet and in the more general case of doing category theory in Mathlib.

Call a construction "u-flexible" if it relates objects in different universes, and "u-rigid" if it demands that the objects it relates have the same universe(s). So, for example, the type Functor C D is u-flexible in C and D, since C and D can live in different universes, but the hom (.of C) ⟶ (.of D) in Cat is u-rigid, since both categories must live in the same universe.

Note that, in this case, the hom in Cat is in some sense the u-rigidification of the u-flexible Functor; conversely, we'll say Functor is a u-relaxation of hom. This isn't intended to be precise, but just to give us some terminology for the situation where two constructions are expressing the same facts but with different universe constraints.

Importantly for us, Equivs among types are u-flexible, and u-rigidify to Isos in the category on Type _.

But, interestingly, I can't see anything which is the u-relaxation of Isos in the (1-)category on Cat, which would be a StrictEquivalence. (Am I missing it?)

Equivalence is u-flexible, but of course is 2-categorical, and does not correspond to the u-rigid Isos in the 1-category Cat that we actually have in Mathlib.

It seems like this is in some part responsible for the universe issues seen earlier when attempting to use simplexIsNerve: the Isos we were composing all needed to relate items in the same universe, so nerve (Fin _) had to be lifted somehow. We didn't have the option of u-flexibly composing StrictEquivalences, and then rigidifying by constructing an Iso out of the composite (which hopefully would happen to have the right universe parameters at either end).

Therefore, we currently have to "frontload" the universe polymorphism with ULiftFin because we must rigidify before putting our pieces together with Iso.trans.

But if we flip the script and put u-flexible pieces together instead...then maybe we can then just rigidify at the end, when we need to. u-rigidifying "at the end" (which, if your endpoints are in the right universe already, might mean "not at all"!) sounds like it might be nicer than having to go back and make every individual factor universe polymorphic (e.g. Fin → ULiftFin) only after we realize it's needed.

This approach would of course mean getting StrictEquivalence right: there are at least 3 broad approaches for implementing it, with choices to make within each. (Having tried it for a bit, none of them seem to be obviously nice out of the gate...) We'd also want some API for the right sort of ULifting here to help us u-rigidify on demand.

The obvious red flag is that StrictEquivalences are not very category-minded! But we are already implicitly using them in Mathlib "accidentally" simply by talking about Isos in the 1-category Cat—we're just not also using them u-flexibly, unlike with other constructions.

[Thomas Murrills]

I could of course be wrong about this approach! Maybe there are insurmountable obstacles, or inconveniences down the line. But I thought I'd propose it with a grain of salt.

The motto "prefer constructing u-flexible relationships" would also provide an answer to the question of how best to construct isos among types, by the way: it would tell us to prefer Equiv, then turn it into an Iso only when necessary.

Ideally, we can build ways to easily interconvert between u-rigid and u-flexible constructions on the fly so that no finicky management needs to be done at all (this is what I'm secretly hoping). Moreover, it would be great to say not only "prefer u-flexible relationships", but "prefer u-flexible relationships between objects in the lowest possible universe in cases where the higher universes are all obtained through ULifting of some sort". Whether this is a good idea depends on the strength of the ulifting API, I think.

[Emily Riehl]

This is very interesting. It would be great if someone who has more interest handling universe issues would comment. Maybe you should repost this on the mathlib channel?

[Emily Riehl]

One thought: there is an analogous u-rigid notion of equivalence, namely equivalence in a bicategory. But the notion of equivalence of types isn't defined this way. Soon though the infinity-cosmos project will give us various (equivalent) notions of equivalence of quasi-categories, all of which will be u-rigid.

[Kevin Buzzard]

Thomas Murrills said:

This approach would of course mean getting StrictEquivalence right: there are at least 3 broad approaches for implementing it, with choices to make within each. (Having tried it for a bit, none of them seem to be obviously nice out of the gate...) We'd also want some API for the right sort of ULifting here to help us u-rigidify on demand.

If you do ask in #mathlib4 then maybe also post some of your suggestions that you tried here?