Directed graphs

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

Created on 2022-02-10.
Last modified on 2023-06-10.

module graph-theory.directed-graphs where
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels


A directed graph consists of a type of vertices equipped with a binary, type valued relation of edges. Alternatively, one can define a directed graph to consist of a type V of vertices, a type E of edges, and a map E → V × V determining the source and target of each edge.

To see that these two definitions are equivalent, recall that -types preserve equivalences and a type family is equivalent to by type duality. Using these two observations we make the following calculation:


Directed-Graph : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Directed-Graph l1 l2 = Σ (UU l1)  V  V  V  UU l2)

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

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

  edge-Directed-Graph : (x y : vertex-Directed-Graph)  UU l2
  edge-Directed-Graph = pr2 G

  total-edge-Directed-Graph : UU (l1  l2)
  total-edge-Directed-Graph =
    Σ ( vertex-Directed-Graph)
      ( λ x  Σ vertex-Directed-Graph (edge-Directed-Graph x))

  source-total-edge-Directed-Graph :
    total-edge-Directed-Graph  vertex-Directed-Graph
  source-total-edge-Directed-Graph = pr1

  target-total-edge-Directed-Graph :
    total-edge-Directed-Graph  vertex-Directed-Graph
  target-total-edge-Directed-Graph e = pr1 (pr2 e)

  edge-total-edge-Directed-Graph :
    (e : total-edge-Directed-Graph) 
      ( source-total-edge-Directed-Graph e)
      ( target-total-edge-Directed-Graph e)
  edge-total-edge-Directed-Graph e = pr2 (pr2 e)

  direct-predecessor-Directed-Graph :
    vertex-Directed-Graph  UU (l1  l2)
  direct-predecessor-Directed-Graph x =
    Σ vertex-Directed-Graph  y  edge-Directed-Graph y x)

  direct-successor-Directed-Graph :
    vertex-Directed-Graph  UU (l1  l2)
  direct-successor-Directed-Graph x =
    Σ vertex-Directed-Graph (edge-Directed-Graph x)

Alternative definition

module alternative where

  Directed-Graph' : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
  Directed-Graph' l1 l2 = Σ (UU l1) λ V  Σ (UU l2)  E  (E  V) × (E  V))

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

    vertex-Directed-Graph' : UU l1
    vertex-Directed-Graph' = pr1 G

    edge-Directed-Graph' : UU l2
    edge-Directed-Graph' = pr1 (pr2 G)

    source-edge-Directed-Graph : edge-Directed-Graph' -> vertex-Directed-Graph'
    source-edge-Directed-Graph = pr1 (pr2 (pr2 G))

    target-edge-Directed-Graph : edge-Directed-Graph' -> vertex-Directed-Graph'
    target-edge-Directed-Graph = pr2 (pr2 (pr2 G))
module equiv {l1 l2 : Level} where
  open alternative

  Directed-Graph-to-Directed-Graph' :
    Directed-Graph l1 l2 -> Directed-Graph' l1 (l1  l2)
  pr1 (Directed-Graph-to-Directed-Graph' G) = vertex-Directed-Graph G
  pr1 (pr2 (Directed-Graph-to-Directed-Graph' G)) =
    Σ ( vertex-Directed-Graph G)
      ( λ x  Σ (vertex-Directed-Graph G) λ y  edge-Directed-Graph G x y)
  pr1 (pr2 (pr2 (Directed-Graph-to-Directed-Graph' G))) = pr1
  pr2 (pr2 (pr2 (Directed-Graph-to-Directed-Graph' G))) = pr1  pr2

  Directed-Graph'-to-Directed-Graph :
    Directed-Graph' l1 l2 -> Directed-Graph l1 (l1  l2)
  pr1 (Directed-Graph'-to-Directed-Graph (V , E , st , tg)) = V
  pr2 (Directed-Graph'-to-Directed-Graph (V , E , st , tg)) x y =
    Σ E  e  (Id (st e) x) × (Id (tg e) y))

Recent changes