The category paths on a quiver. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
C is a quiver,
paths C is the category of paths.
When the quiver is itself a category #
path_composition : paths C ⥤ C.
We check that the quotient of the path category of a category by the canonical relation
(paths are related if they compose to the same path) is equivalent to the original category.
A type synonym for the category of paths in a quiver.
The inclusion of a quiver
V into its path category, as a prefunctor.
Any prefunctor from
V lifts to a functor from
Two functors out of a path category are equal when they agree on singleton paths.
A path in a category can be composed to a single morphism.
Composition of paths as functor from the path category of a category to the category.
The canonical relation on the path category of a category:
two paths are related if they compose to the same morphism.
The functor from a category to the canonical quotient of its path category.
The functor from the canonical quotient of a path category of a category
to the original category.
The canonical quotient of the path category of a category
is equivalent to the original category.