nLab reflexive graph

Idea

A graph is reflexive if for each vertex $v$ there is a (specified) edge $v \to v$.

A reflexive quiver has a specified identity edge $i_X: X \to X$ on each object (vertex) $X$.

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.

Properties

Proposition

The category of reflexive directed graphs $RefGph$, i.e., reflexive quivers, equipped with the functor $U: RefGph \to Set$ which sends a graph to its set of edges, is monadic over $Set$.

Proof

$RefGph$ is the category of functors $R \to Set$ where $R$ is the walking reflexive fork, consisting of two objects $0, 1$ and generated by arrows $i: 0 \to 1$ and $s, t: 1 \to 0$ subject to $s i = 1_0 = t i$ and no other relations. This $R$ is in turn the Cauchy completion of a monoid $M$ consisting of two elements $e_0 = i s, e_1 = i t$ and an identity, with multiplication $e_0 e_0 = e_0 = e_1 e_0$ and $e_1 e_1 = e_1 = e_0 e_1$, and therefore $RefGph$ is equivalent to the category of functors $M \to Set$, i.e., the category of $M$-sets $Set^M$. This is the category of algebras of the monad $M \times -$ whose monad structure is induced from the monoid structure of $M$.

$Cat$ is monadic over $RefGph$ and $RefGph$ is monadic over $Set$ but $Cat$ is not monadic over $Set$; this is a nice example of how the relation ‘being monadic over’ is not transitive.

In dependent type theory

In dependent type theory, a graph $(A; x:A, y:A \vdash R(x, y))$ is reflexive if

• it comes with a family of elements $x:A \vdash \mathrm{refl}_A^R(x):R(x, x)$.
• it comes with a family of functions $\mathrm{idtofam}(x, y):(x =_A y) \to R(x, y)$.

These two definitions are the same. From $\mathrm{refl}_A^R(x)$, we can inductively define $\mathrm{idtofam}(x, y)$ on reflexivity:

$$\mathrm{idtofam}(x, x)(\mathrm{refl}_A(x)) \coloneqq \mathrm{refl}_A^R(x)$$

From $\mathrm{idtofam}(x, y)$ we define $\mathrm{refl}_A^R(x)$ to be

$$\mathrm{refl}_A^R(x) \coloneqq \mathrm{idtofam}(x, x)(\mathrm{refl}_A(x))$$

Related concepts

• reflexive relation

• univalent reflexive graph

References

Classifying the closed symmetric monoidal-structures on the category of reflexive graphs:

• Krzysztof Kapulkin, Nathan Kershaw: Closed symmetric monoidal structures on the category of graphs, Theory and Applications of Categories 41 23 (2024) 760-784 [tac:41-23, arXiv:2310.00493]