Raising universe levels of directed graphs

module graph-theory.raising-universe-levels-directed-graphs where

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.raising-universe-levels
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.equivalences-directed-graphs
open import graph-theory.walks-directed-graphs

Idea

We raise the universe levels of directed graphs by raising the universe levels of the vertices and the edges.

Definition

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

  vertex-raise-Directed-Graph : UU (l1 ⊔ l3)
  vertex-raise-Directed-Graph = raise l3 (vertex-Directed-Graph G)

  equiv-vertex-compute-raise-Directed-Graph :
    vertex-Directed-Graph G ≃ vertex-raise-Directed-Graph
  equiv-vertex-compute-raise-Directed-Graph =
    compute-raise l3 (vertex-Directed-Graph G)

  vertex-compute-raise-Directed-Graph :
    vertex-Directed-Graph G → vertex-raise-Directed-Graph
  vertex-compute-raise-Directed-Graph =
    map-equiv equiv-vertex-compute-raise-Directed-Graph

  edge-raise-Directed-Graph :
    (x y : vertex-raise-Directed-Graph) → UU (l2 ⊔ l4)
  edge-raise-Directed-Graph (map-raise x) (map-raise y) =
    raise l4 (edge-Directed-Graph G x y)

  equiv-edge-compute-raise-Directed-Graph :
    (x y : vertex-Directed-Graph G) →
    edge-Directed-Graph G x y ≃
    edge-raise-Directed-Graph
      ( vertex-compute-raise-Directed-Graph x)
      ( vertex-compute-raise-Directed-Graph y)
  equiv-edge-compute-raise-Directed-Graph x y =
    compute-raise l4 (edge-Directed-Graph G x y)

  edge-compute-raise-Directed-Graph :
    (x y : vertex-Directed-Graph G) →
    edge-Directed-Graph G x y →
    edge-raise-Directed-Graph
      ( vertex-compute-raise-Directed-Graph x)
      ( vertex-compute-raise-Directed-Graph y)
  edge-compute-raise-Directed-Graph x y =
    map-equiv (equiv-edge-compute-raise-Directed-Graph x y)

  raise-Directed-Graph : Directed-Graph (l1 ⊔ l3) (l2 ⊔ l4)
  pr1 raise-Directed-Graph = vertex-raise-Directed-Graph
  pr2 raise-Directed-Graph = edge-raise-Directed-Graph

  compute-raise-Directed-Graph :
    equiv-Directed-Graph G raise-Directed-Graph
  pr1 compute-raise-Directed-Graph = equiv-vertex-compute-raise-Directed-Graph
  pr2 compute-raise-Directed-Graph = equiv-edge-compute-raise-Directed-Graph

  walk-raise-Directed-Graph :
    (x y : vertex-raise-Directed-Graph) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  walk-raise-Directed-Graph = walk-Directed-Graph raise-Directed-Graph

  equiv-walk-compute-raise-Directed-Graph :
    {x y : vertex-Directed-Graph G} →
    walk-Directed-Graph G x y ≃
    walk-raise-Directed-Graph
      ( vertex-compute-raise-Directed-Graph x)
      ( vertex-compute-raise-Directed-Graph y)
  equiv-walk-compute-raise-Directed-Graph =
    equiv-walk-equiv-Directed-Graph G
      raise-Directed-Graph
      compute-raise-Directed-Graph

  walk-compute-raise-Directed-Graph :
    {x y : vertex-Directed-Graph G} →
    walk-Directed-Graph G x y →
    walk-raise-Directed-Graph
      ( vertex-compute-raise-Directed-Graph x)
      ( vertex-compute-raise-Directed-Graph y)
  walk-compute-raise-Directed-Graph =
    map-equiv equiv-walk-compute-raise-Directed-Graph