Generalizing `Discrete`?

Stream: mathlib4

[Robert Maxton]

I've run into a use case where it would be useful to be able to make a Discrete category whose morphisms live in a different universe level than its objects. Specifically, I'm generalizing the construction of explicit limits of size v in Cat.{v, v} to limits of size w in Cat.{v, u} with w ≤ u, v, and in the process I ended up wanting a proof that objectspreserves all limits in Cat.{v, u}, even the ones too big to fit.

In the process of completing that proof, I ended up rolling my own version of Discrete:

universe v u
@[ext]
structure Discrete' (α : Type u) where
  as : let _ := ULift.{w} α; α

namespace Discrete'
universe v' u' v₁ u₁ v₂ u₂

variable {α : Type u}

@[simps id]
instance : Category.{v, u} (Discrete' α) where
  Hom X Y := ULift (PLift (X.as = Y.as))
  id X := ULift.up (PLift.up rfl)
  comp := by rintro ⟨⟩ ⟨⟩ ⟨⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩; exact ⟨⟨rfl⟩⟩
-- ...

The only difference between this and the original Discrete is that Discrete is a SmallCategory, thus has morphisms in Type u, whereas this has morphisms in some arbitraryType v. This allows me to, for example, easily make images of simple types in whatever Cat level I like, rather than being restricted to homogenous universe levels.

[Robert Maxton]

@Kim Morrison Inspection of ULiftHom seems to have resolved the dilemma we were having in office hours; I'm going to go find out if this breaks anything in my local Mathlib if I change Discrete to this

[Robert Maxton]

... And it seems the answer is "no", though I haven't tried building all of Mathlib. In fact I barely had to change anything; we don't often use universe levels with Discrete in the current definition, so there's very little to change when adding an extra level.

[Robert Maxton]

Hm. Okay, a few things popped up when I ran CI over it, but still just a few here and there. It does seem like there might be a market for DiscreteSmall, defined as the original definition, though. Or some other abbreviated sensible default