Design question: `asFunctor.{w}` or `... ⋙ uliftFunctor`?

Stream: mathlib4

[Robert Maxton]

I'm finishing up limits and colimits in Quiv.{v, u}; I have a working version and am now refactoring/cleaning it up to be presentable for Mathlib.

One thing I'd like to check for opinions on: The easiest way to create (co)limits in Quiv is by writing the category as a presheaf category and porting over limits that way. I expect that in general, quite a lot of categorical machinery will be easiest provided by making use of the general richness/well-behavedness of presheaf categories, so I would like this machinery to be fluid and easy to use.

Unfortunately, when v the universe level of the edges does not match u the universe level of the vertices, things get messy, and Quiv ceases to be equivalent to the entirety of the corresponding presheaf category, greatly complicating matters. To work around this, I have created machinery for working with the full subcategory of functors that happen to be v, u-small when represented as a quiver.

I now have a choice: I can either define

asFunctor.{w, v, u} : Quiv.{v, u} ⥤ WalkingQuiver ⥤ Type max w v u

with an extra universe level w, so that the underlying definition can work natively with functors into a larger level of Type than strictly required. This allows the core machinery to work with many universe levels directly, but moderately complicates the resulting implementation as a result. It also means that you gain less benefit from working in the usual simpler case of u = v; the complexity of having heterogenous universe levels bleeds over.

Alternatively, I can hardcode asFunctor to be as small as it can be:

asFunctor.{v, u} : Quiv.{v, u} ⥤ WalkingQuiver ⥤ Type max v u

and instead prove lemmas about asFunctor ⋙ whiskeringRight.obj uliftFunctor and similar contortions, ultimately culminating in an equivalence that has the same universe polymorphism features as in the first option. This in some sense results in a cleaner, better-structured library at a higher level, which also allows users to use the simpler homogenous-universe-level code when applicable; but it also results in harder to read, harder to use definitions in terms of heavily nested compositions, as well as cluttering up search results with extra internal implementation details.

One of these is already coded; I got halfway through refactoring it into the other before starting to reconsider.

Thoughts/opinions?