Reflexive graphs

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

Created on 2022-02-10.
Last modified on 2024-12-03.

module graph-theory.reflexive-graphs where
Imports 
open import foundation.binary-dependent-identifications
open import foundation.dependent-pair-types
open import foundation.identity-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 =
  Σ ( Directed-Graph l1 l2)
    ( λ G → (x : vertex-Directed-Graph G) → edge-Directed-Graph G x x)

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

  directed-graph-Reflexive-Graph : Directed-Graph l1 l2
  directed-graph-Reflexive-Graph = pr1 G

  vertex-Reflexive-Graph : UU l1
  vertex-Reflexive-Graph = vertex-Directed-Graph directed-graph-Reflexive-Graph

  edge-Reflexive-Graph : vertex-Reflexive-Graph → vertex-Reflexive-Graph → UU l2
  edge-Reflexive-Graph = edge-Directed-Graph directed-graph-Reflexive-Graph

  refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x
  refl-Reflexive-Graph = 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

  binary-dependent-identification-refl-Reflexive-Graph :
    {x y : vertex-Reflexive-Graph} (p : x ＝ y) →
    binary-dependent-identification edge-Reflexive-Graph p p
      ( refl-Reflexive-Graph x)
      ( refl-Reflexive-Graph y)
  binary-dependent-identification-refl-Reflexive-Graph =
    binary-dependent-identification-refl-Reflexive-Relation
      edge-reflexive-relation-Reflexive-Graph

See also

Recent changes