Commit 2026-01-27 01:42 0e16bffe

refactor: Restrict quiver homs to Type* (#34228) The current definition of Quiver allows morphisms to be in Prop. The docstring explicitly mentions that if you want to use Props as morphisms, you can do this with Quiver.{0}. But in fact there are only two occurrences of the string Quiver.{0} in mathlib, one in the docstring of Quiver, and one in the docstring of Digraph explaining why Quiver.{0} was not suitable for digraphs (because Quiver is a class); the definition of Digraph is precisely Quiver.{0} but as a structure. In contrast, there are many many occurrences of Quiver.{v + 1} in mathlib, all of which can be removed with this refactor. It turns out that there is actually one Quiver.{0} in Mathlib: Matrix.toQuiver associates a Prop-valued quiver to a matrix with entries in a linearly ordered ring. There are two possible fixes here; I use PLift which was the easier one; another possibility is to make Matrix.toDigraph instead.