A graph is reflexive if for each vertex there is a (specified) edge .
A reflexive quiver has a specified identity edge on each object (vertex) .
The free category on a reflexive quiver has the same objects, identity morphisms corresponding to the identity edges, and non-identity morphisms consisting of paths of non-identity edges.
The category of reflexive directed graphs , i.e., reflexive quivers, equipped with the functor which sends a graph to its set of edges, is monadic over .
is the category of functors where is the walking reflexive fork, consisting of two objects and generated by arrows and subject to and no other relations. This is in turn the Cauchy completion of a monoid consisting of two elements and an identity, with multiplication and , and therefore is equivalent to the category of functors , i.e., the category of -sets . This is the category of algebras of the monad whose monad structure is induced from the monoid structure of .
is monadic over and is monadic over but is not monadic over ; this is a nice example of how the relation ‘being monadic over’ is not transitive.
In dependent type theory, a graph is reflexive if
These two definitions are the same. From , we can inductively define on reflexivity:
From we define to be
Classifying the closed symmetric monoidal-structures on the category of reflexive graphs:
Last revised on October 7, 2024 at 10:54:06. See the history of this page for a list of all contributions to it.