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
.