Paths in quivers #
Given a quiver
V, we define the type of paths from
a : V to
b : V as an inductive
family. We define composition of paths and the action of prefunctors on paths.
G.path a b is the type of paths from
b through the arrows of
An arrow viewed as a path of length one.
The length of a path is the number of arrows it uses.
Composition of paths.
Turn a path into a list. The list contains
a at its head, but not
b a priori.
The image of a path under a prefunctor.