Place for 'shapes' of simple quivers and categories.

Stream: mathlib4

[Robert Maxton]

Having finished one project I am returning to my previous PRs, in particular #24540 where I define the empty, vertex, point, and interval quivers. I did this in part because I personally find dealing with ULift and ULiftHom quite annoying when embedded into bundled objects I have to use frequently, ULiftHom especially as it tends to lead to 'defeq abuse' problems on objects; all the quivers in that file are defined so that they can be given a specific pair of universe levels for objects and morphisms.

This does mean that there is some overlap with existing objects, and some uncertainty as to where exactly that file belongs. The Empty quiver could just as easily be defined as a category, for example, and its only difference with the existing category instance on PEmpty is that, again, it can be given an explicit universe level for its morphisms. The only objects that have to be quivers are Vertex (the quiver with one vertex and no edges at all) and Interval (the quiver with two vertices and the edge between them), as they lack identities; everything else could, I suppose, be put into Cat instead. Not coincidentally, those are the ones I consider most important from that PR, as I use them later in the project and they can't easily be replaced by existing objects.

Where should these objects go? @Joël Riou , you had some opinions on the matter when I first made the PR?

[Aaron Liu]

Robert Maxton said:

The Empty quiver could just as easily be defined as a category, for example, and its only difference with the existing category instance on PEmpty is that, again, it can be given an explicit universe level for its morphisms.

Why isn't that possible for the category?

[Robert Maxton]

Same reason my PR for doing it for Discrete got mostly-rejected: it's not impossible, but it results in universe level unification issues down the line in a bunch of uses that don't actually need the capability and would rather not be concerned with it. Personally I would rather live with it but shrug.

[Joël Riou]

We used to have versions of basic shapes of categories with extraneous universe parameters (e.g. there was one WalkingParallelPair in each universe). It was terrible. Since https://github.com/leanprover-community/mathlib3/pull/15067 we have only one of these, in Type 0, and the category theory works much better now. I would not like we revert this design choice by introducing irrelevant universe parameters again when dealing with unbundled objects like categories or quivers.
What I would suggest is defining types with Quiver/Category instances with the lowest possible universe only.
If you need to work in Quiv or Cat, then you may define terms by ulifting these constructions to the expected universes.

[Robert Maxton]

In that case, why not just make bundled Cat and Quiv objects with the right universe levels? Again, I don't like the ULift option; not only does it add a nontrivial amount of mental noise (especially since rcases doesn't respect cases_eliminator), but ULiftHom actually introduces defeq problems that e.g. make simp lemmas not fire

[Joël Riou]

There have been a few instances where not defining the unbundled objects first made things more ackward afterwards. There may be issues with ulift, but I think it is better to improve the API.
For example, in the context of simplicial sets, ulift appears in the definition of the standard simplex in SSet.{u}, but the API makes it so that most of the times we do not even have to think that there is a ulift.

[Robert Maxton]

Mm. The issue is that to my knowledge, you can't actually make API that rcases and casesm, and their derived tactics, will recognize. For some purposes, that might not be a total dealbreaker, as I can probably make do with 'opaque' lift/desc defs and associated lemmas, but esp. with the walking quiver there are proofs that are currently best done via rintro that will break if I have to use a 'non-canonical' matcher -- in particular, ULiftHom.

[Joël Riou]

Let us say you define a certain quiver C : Type 0 using inductive types, and you want to compute the type of prefunctors from C to a quiver D in any universe. You may first do that with the universe polymorphic API of quivers. Then, in order to translate this into a computation of morphisms in Quiv, you just need to know that prefunctors from C or from the ulifted version of C can be identified: as this works for any C, there is no need to do induction on C or the type of morphisms in C.