is ulift necessary in simplex_category?

Stream: general

[Joël Riou]

In algebraic_topology.simplex_category and simplicial_object, we have these definitions

def simplex_category := ulift.{u} ℕ

variables (C : Type u) [category.{v} C]
def simplicial_object := simplex_category.{v}ᵒᵖ ⥤ C

Is there any reason why simplex_category is not just defined as ℕ (or as an obviously equivalent type which would not depend on a universe parameter)? (Was it something necessary in the early development of mathlib when universe parameters were not as practical as they are now?) Would not it be better to remove this ulift?

This is annoying because when we study the functoriality of categories of simplicial objects, the whiskering functor is defined only for functors C ⥤ D for which both categories have the same universe for the maps.

In comparison, we do not have this problem with homological_complex: in algebra.homology.additive, map_homological_complex does not have this restriction.

[Adam Topaz]

@Joël Riou Back in the day we had additional universe restrictions in the definitions of (co)limits, and at some point there was no ulift. We added the ulift to the simplex category in order to obtain (co)limits of simplicial objects in terms of (co)limits of functors. It's possible that, after @Andrew Yang 's change to the universes in the (co)limit library, it is now possible to remove ulift. On the other hand, I do think it could be worthwhile to have a universe polymorphic simplex_category, so we may consider either leaving the ulift there, or redefining simplex_category altogether with some bespoke typees.

[Joël Riou]

@Adam Topaz Thanks. Indeed, if we remove the ulift, it seems to me that the has_limits and has_colimits instances are automatically obtained from category_theory.limits.functor_category. Then, would not it be better to change back simplex_category as equivalent to ℕ, and then use the general constructions you did in category_theory.category.uliftto ulift both objects and morphisms to a chosen universe (if this is really needed)? (Actually, it seems to me that the code in simplex_category kind of duplicates the code in category.ulift.) This would not be very high in my priority list, but I could try to do it before I PR the functoriality of the Dold-Kan equivalence (with respect to additive functors between abelian categories).

[Adam Topaz]

@Joël Riou Yes, I think what you propose could be a good approach, but let's also ask for input from @Johan Commelin and @Scott Morrison

[Johan Commelin]

Yup, I agree that the ulift can now probably be stripped out again. That seems like the natural way forward to me, because it cleans up the definition.

[Scott Morrison]

Yes, now that the universe restrictions on limits have been removed, the ulift is just noise. Users can ulift the simplex category in particular circumstances that it becomes necessary, if such exist.

[Joël Riou]

I have removed this ulift in PR #13183.