Digraph vs Quiver.{0}

Stream: mathlib4

[Oliver Nash]

Mathlib contains both docs#Quiver (with a moderate API) and docs#Digraph (with a small API) but mathematically Quiver.{0} is the same as Digraph.

So we could do any of:

1. Continue with both, living with the duplication
2. Make Digraph an abbrev for Quiver.{0} (and write some custom API for this case)
3. Something else

Has anyone thought about this?

[Shreyas Srinivas]

(deleted)

[Robin Arnez]

I guess Quiver being a class vs Digraph being a structure might be a relevant discrepancy?

[Kim Morrison]

(Noting also that Category extends CategoryStruct which extends Quiver. I don't know whether "un-classing" Quiver would cause a problem there.)

[Kevin Buzzard]

In #34228 I try a completely different solution which is simply to change Sort v to Type v in the definition of quiver, i.e. make our old Quiver.{0} not exist any more, because we have Digraph. It makes mathlib much better (a lot of our theory of quivers only works for types, it turns out, and right now we use the slightly clunky fix Quiver.{v+1} everywhere). The diff is very pleasing, but it has one catch, in that just over the last few months we merged Matrix.toQuiver which constructs a digraph from a matrix, but we used quiver because it had more API :-/ Right now I fixed it with a PLift hack.

[Junyan Xu]

Maybe rename Quiver to SQuiver and define Quiver.{v} = SQuiver.{v+1} and Digraph = SQuiver.{0}

[Yaël Dillies]

Please don't. Digraph is acquiring a support set, cf #33466

[Junyan Xu]

1. Continue with both, living with the duplication

Actually we've always been living with the duplications docs#And and docs#Prod, etc.
(docs#PProd subsumes both but is rarely used; by that naming convention SQuiver should be PQuiver)

[Matteo Cipollina]

a bit more context also here #mathlib4 > RFC: Quiver refactor

[Kevin Buzzard]

PProd doesn't subsume And because it can't return a Prop.

[Aaron Liu]

it is possible to make a universe polymorphic product type with signature Sort u → Sort v → Sort (max u v) and this would subsume both And and Prod

[Junyan Xu]

Doesn't work:

universe u v
structure Prod' (α : Sort u) (β : Sort v) : Sort max u v where
  left : α
  right : β
/- Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort (max u v)

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _` -/

[Junyan Xu]

I recall it used to work in Lean 3 (I think I also see imax more often those days); I recall there are some changes to the kernel in between but I can't point to the PR(s)

[Kevin Buzzard]

The reason this doesn't show up with Quiver (and Category) is that Quiver involves Type u so can never be a Prop itself.

[Junyan Xu]

The universe of docs#Quiver is pretty: Type max u v. It's the universe of CategoryTheory.CategoryStruct that is ugly (Type max u (v+1)). Should we change (generalize) the latter instead? That would also eliminate the ULift hack we use to define the category associated to a preorder.

[Aaron Liu]

Junyan Xu said:

Doesn't work:

you aren't trying hard enough:

universe u v
set_option genInjectivity false in
set_option genSizeOf false in
set_option bootstrap.inductiveCheckResultingUniverse false in
inductive Prod' (α : Sort u) (β : Sort v) : Sort (max u v) where
  | mk (left : α) (right : β) : Prod' α β

[Kevin Buzzard]

Junyan Xu said:

Should we change (generalize) the latter instead?

I don't think so. I don't think you can have everything pretty. For example, for large categories right now, u=v+1 and our "ugly" type simplifies to Type (v+1).

[Kevin Buzzard]

Aaron Liu said:

you aren't trying hard enough:

I suspect that with all those set_options you might be trying a little too hard (at least as far as mathlib is concerned!)

[Junyan Xu]

Can you prove false with bootstrap.inductiveCheckResultingUniverse false?
(Update: I tried and it still checks the specified universe is large enough.)

[Aaron Liu]

Kevin Buzzard said:

Aaron Liu said:

you aren't trying hard enough:

I suspect that with all those set_options you might be trying a little too hard (at least as far as mathlib is concerned!)

yeah it's definitely not worth the trouble

[Aaron Liu]

Junyan Xu said:

Can you prove false with bootstrap.inductiveCheckResultingUniverse false?

I sure hope not, given that it's used in prelude for PEmpty and PUnit

[Aaron Liu]

src#PEmpty, src#PUnit

[Kevin Buzzard]

In the past we tried to change Category to accept Sort-valued morphisms and the result is just the opposite of #34228 -- lots of +1s and fighting.

[Chris Henson]

Kevin Buzzard said:

In the past we tried to change Category to accept Sort-valued morphisms and the result is just the opposite of #34228 -- lots of +1s and fighting.

Which is unfortunate, because it makes categorical semantics for lambda calculi very difficult downstream. You either do intrinsic typing judgements in Type (shutting you out of much of the idiomatic formalization techniques unless you use tactics to construct data) or have to wrangle with universe lifting. I've still not gotten to a point where I have a solution I really like to the point of putting it in CSLib.

[Junyan Xu]

Apparently Quiver is used in 195 files and Kevin's PR only removes +1 from 20 of them.
Was Sophie's problem mainly due to the Category/Quiver mismatch? If so then changing either should solve the problem.

[Kevin Buzzard]

I don't think generalizing Category is at all feasible -- as I say it's been tried before and it was a failure (although this might have been in Lean3?). Sophie was just frustrated because she was getting obscure universe errors due to the Category/Quiver mismatch and I thought I'd experiment with changing Quiver to see if we were really using it. I don't have a strong argument for merging #34228 other than the fact that it establishes the symmetry.

[Junyan Xu]

Can you point to previous attempts (branch/PR)? Apparently the design decision is not documented in docstrings.

[Chris Henson]

It was Lean 3, I can find it...

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib3/pull/1256 and https://github.com/leanprover-community/mathlib3/pull/1122 and https://github.com/leanprover-community/mathlib3/pull/1412 and #new members > ✔ Universe Restriction on CategoryTheory.Category @ 💬

[Chris Henson]

Also here: #mathlib4 > categories with morphisms in Prop where I asked more recently

[Junyan Xu]

Indeed from mathlib3#1412 I see a lot of +1 are needed (in 47 files, back then) if we switch morphisms back from Type to Sort.
mathlib3#824 was the PR that switched both objects and morphisms to Sort.

[Shreyas Srinivas]

Yaël Dillies said:

Please don't. Digraph is acquiring a support set, cf #33466

To add, digraph will sooner or later acquire graph theoretic API. I already discussed an improved definition of graphs walks in a graph theory thread. This is to address the concern that there isn’t much API for digraph. It’s a historical accident. There is also a theoretical possibility to generalise pieces of the SimpleGraph API to digraphs and use them for SimpleGraphs by extending them from Digraphs.

[Adam Topaz]

Kevin’s PR (#34228) was just assigned to me. I think this change is a good idea and I’m inclined to merge it very soon, but I will hold off for a few days in case there are any convincing objections.