Universe issues: ulifting from low-u data

Stream: Infinity-Cosmos

[Thomas Murrills]

Some relevant constructions like Δ[n] are universe polymorphic, but nonetheless get all their data from a single low universe level.

For example, with ∆[n] := stdSimplex.obj ⦋n⦌, we can see that

def stdSimplex : CosimplicialObject SSet.{u} :=
  yoneda ⋙ uliftFunctor

and when printing the universe levels, we see

def SSet.stdSimplex.{u} : CosimplicialObject.{u, u + 1} SSet.{u} :=
  Functor.comp.{0, 0, u, 0, 1, u + 1} yoneda.{0, 0} uliftFunctor.{u, 0}

i.e., all of the higher universe compatibility comes from uliftFunctor—which makes sense when we think through how yoneda decides where to live. Its universe levels here come from those of SimplexCategory (which demands one ulift, but not necessarily any more!).

In e.g. the case of Δ[n], we can express this internally as (SSet.uliftFunctor.obj Δ[n]) ≅ Δ[n] (with appropriate universe freedom):

def uliftSimplexIsoSimplex (n : ℕ) : (Δ[n] ⋙ uliftFunctor.{u,v}) ≅ Δ[n] :=
  NatIso.ofComponents fun _ ↦ Equiv.toIso <|
    Equiv.ulift.trans Equiv.ulift |>.trans Equiv.ulift.symm

Similarly, we have nerve (ULiftCat.{v', u'} C) ≅ SSet.uliftFunctor.obj.{max u' v'} <| nerve C (i.e., if all of a category's data comes from a lower universe level, so does nerve _'s):

def nerveULift.{v',u'} {C : Type u} [Category.{v} C] :
    nerve (ULiftCat.{v', u'} C) ≅ SSet.uliftFunctor.obj.{max u' v'} <| nerve C :=
  NatIso.ofComponents fun _ ↦ Equiv.toIso <|
    Functor.upRightEquiv.symm.trans Equiv.ulift.symm

(where I'm using Functor.upRightEquiv : X ⥤ Y ≃ X ⥤ ULiftCat Y from my own bespoke ulifting API for now).

But proving individual things like this—and constructing the right squares, e.g. chaining Δ[0] ≅ SSet.uliftFunctor.obj Δ[0], SSet.uliftFunctor.obj Δ[0] ≅ SSet.uliftFunctor.obj (nerve (Fin 1)) (which we have for free since SSet.uliftFunctor is a functor), and SSet.uliftFunctor.obj (nerve (Fin 1)) ≅ nerve (ULiftCat (Fin 1)), inserting the right symms—is tedious.

I'm wondering if some metaprogramming can be done to move things between universe levels easily, so that

1. we can generate the "ulift isomorphisms" automatically, e.g. by attaching some attribute (@[ulifts]?) to stdSimplex.obj and nerve when declared
2. we can insert those isomorphisms automatically when we need to move between universe levels. Ideally, we could just write something like u(simplexIsNerve 0) and it would modify the universes as appropriate for the expected type.

One part of this issue, imo, is "freezing" (and rigidifying!) the universe levels when moving inside Cat, and I'd hope that the above would also help us move more fluidly between Cat data at different universes somehow.