This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Reflexive graphs

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

open import graph-theory.directed-graphs

Idea

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

Definition

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)
  where

  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