Reflexive graphs

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

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

module graph-theory.reflexive-graphs where
Imports 
open import foundation.dependent-pair-types
open import foundation.reflexive-relations
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)

  edge-reflexive-relation-Reflexive-Graph :
    Reflexive-Relation l2 vertex-Reflexive-Graph
  pr1 edge-reflexive-relation-Reflexive-Graph = edge-Reflexive-Graph
  pr2 edge-reflexive-relation-Reflexive-Graph = refl-Reflexive-Graph

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

See also

Recent changes