Dependent directed graphs

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

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

open import graph-theory.directed-graphs

Idea

Consider a directed graph A. A dependent directed graph B over A consists of:

  • A family B₀ : A₀ → 𝒰 of vertices
  • A family B₁ : (x y : A₀) → A₁ x y → B₀ x → B₀ y → 𝒰 of binary relations between the types of vertices B₀, indexed by the type of edges A₁ in A.

To see that this is a sensible definition of dependent directed graphs, observe that the type of directed graphs itself is equivalent to the type of dependent directed graphs over the terminal directed graph. Furthermore, graph homomorphisms into the universal directed graph are equivalent to dependent directed graphs.

Definitions

Dependent directed graphs

Dependent-Directed-Graph :
  {l1 l2 : Level} (l3 l4 : Level) → Directed-Graph l1 l2 →
  UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
Dependent-Directed-Graph l3 l4 A =
  Σ ( vertex-Directed-Graph A → UU l3)
    ( λ B₀ →
      (x y : vertex-Directed-Graph A) →
      edge-Directed-Graph A x y → B₀ x → B₀ y → UU l4)

module _
  {l1 l2 l3 l4 : Level} {A : Directed-Graph l1 l2}
  (B : Dependent-Directed-Graph l3 l4 A)
  where

  vertex-Dependent-Directed-Graph : vertex-Directed-Graph A → UU l3
  vertex-Dependent-Directed-Graph = pr1 B

  edge-Dependent-Directed-Graph :
    {x y : vertex-Directed-Graph A} →
    edge-Directed-Graph A x y →
    vertex-Dependent-Directed-Graph x →
    vertex-Dependent-Directed-Graph y → UU l4
  edge-Dependent-Directed-Graph = pr2 B _ _

Constant dependent directed graphs

module _
  {l1 l2 l3 l4 : Level} (A : Directed-Graph l1 l2) (B : Directed-Graph l3 l4)
  where

  vertex-constant-Dependent-Directed-Graph :
    vertex-Directed-Graph A → UU l3
  vertex-constant-Dependent-Directed-Graph x = vertex-Directed-Graph B

  edge-constant-Dependent-Directed-Graph :
    {x y : vertex-Directed-Graph A} →
    edge-Directed-Graph A x y →
    vertex-constant-Dependent-Directed-Graph x →
    vertex-constant-Dependent-Directed-Graph y → UU l4
  edge-constant-Dependent-Directed-Graph e =
    edge-Directed-Graph B

  constant-Dependent-Directed-Graph : Dependent-Directed-Graph l3 l4 A
  pr1 constant-Dependent-Directed-Graph =
    vertex-constant-Dependent-Directed-Graph
  pr2 constant-Dependent-Directed-Graph _ _ =
    edge-constant-Dependent-Directed-Graph

See also

Recent changes