Reflexive graphs

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-02-10.
Last modified on 2024-04-11.

module graph-theory.reflexive-graphs where
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import graph-theory.directed-graphs


A reflexive graph is a directed graph equipped with a loop edge at every vertex.


Reflexive-Graph : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Reflexive-Graph l1 l2 =
  Σ (UU l1)  V  Σ (V  V  UU l2)  E  (v : V)  E v v))

module _
  {l1 l2 : Level} (G : Reflexive-Graph l1 l2)

  vertex-Reflexive-Graph : UU l1
  vertex-Reflexive-Graph = pr1 G

  edge-Reflexive-Graph : vertex-Reflexive-Graph  vertex-Reflexive-Graph  UU l2
  edge-Reflexive-Graph = pr1 (pr2 G)

  refl-Reflexive-Graph : (x : vertex-Reflexive-Graph)  edge-Reflexive-Graph x x
  refl-Reflexive-Graph = pr2 (pr2 G)

  graph-Reflexive-Graph : Directed-Graph l1 l2
  graph-Reflexive-Graph = vertex-Reflexive-Graph , edge-Reflexive-Graph

See also

Recent changes