# Quivers #

This module defines quivers. A quiver on a type `V`

of vertices assigns to every
pair `a b : V`

of vertices a type `a ⟶ b`

of arrows from `a`

to `b`

. This
is a very permissive notion of directed graph.

## Implementation notes #

Currently `Quiver`

is defined with `arrow : V → V → Sort v`

.
This is different from the category theory setup,
where we insist that morphisms live in some `Type`

.
There's some balance here: it's nice to allow `Prop`

to ensure there are no multiple arrows,
but it is also results in error-prone universe signatures when constraints require a `Type`

.

- Hom : V → V → Sort v
The type of edges/arrows/morphisms between a given source and target.

A quiver `G`

on a type `V`

of vertices assigns to every pair `a b : V`

of vertices
a type `a ⟶ b`

of arrows from `a`

to `b`

.

For graphs with no repeated edges, one can use `Quiver.{0} V`

, which ensures
`a ⟶ b : Prop`

. For multigraphs, one can use `Quiver.{v+1} V`

, which ensures
`a ⟶ b : Type v`

.

Because `Category`

will later extend this class, we call the field `Hom`

.
Except when constructing instances, you should rarely see this, and use the `⟶`

notation instead.

## Instances

Notation for the type of edges/arrows/morphisms between a given source and target in a quiver or category.

## Instances For

- obj : V → W
The action of a (pre)functor on vertices/objects.

The action of a (pre)functor on edges/arrows/morphisms.

A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a `Prefunctor`

.

## Instances For

The identity morphism between quivers.

## Instances For

Notation for a prefunctor between quivers.

## Instances For

Notation for composition of prefunctors.

## Instances For

Notation for the identity prefunctor on a quiver.

## Instances For

The opposite of an arrow in `V`

.

## Instances For

A quiver is thin if it has no parallel arrows.