## Weakly connected components #

For a quiver `V`

, define the type `WeaklyConnectedComponent V`

as the quotient of `V`

by
the relation which identifies `a`

with `b`

if there is a path from `a`

to `b`

in `Symmetrify V`

.
(These zigzags can be seen as a proof-relevant analogue of `EqvGen`

.)

Strongly connected components have not yet been defined.

Two vertices are related in the zigzag setoid if there is a zigzag of arrows from one to the other.

## Instances For

The type of weakly connected components of a directed graph. Two vertices are in the same weakly connected component if there is a zigzag of arrows from one to the other.

## Instances For

The weakly connected component corresponding to a vertex.

## Instances For

A wide subquiver `H`

of `Symmetrify V`

determines a wide subquiver of `V`

, containing an
arrow `e`

if either `e`

or its reversal is in `H`

.