Large higher directed graphs

Content created by Fredrik Bakke.

Created on 2024-03-24.
Last modified on 2024-04-11.

module graph-theory.large-higher-directed-graphs where
Imports 
open import elementary-number-theory.natural-numbers

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.large-binary-relations
open import foundation.raising-universe-levels
open import foundation.unit-type
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.higher-directed-graphs

Idea

A large directed -graph is defined inductively:

  • A large directed -graph is a large collection of vertices.
  • A large directed -graph is a large collection of vertices together with a large binary relation E on the vertices, such that E u v is a (small) directed -graph for all u and v.

Definitions

The structure of a large higher directed graph on a large collection of vertices

data
  is-large-higher-directed-graph
  {α : Level → Level}
  (β γ : Level → Level → Level)
  (V : (l : Level) → UU (α l)) :
  (n : ℕ) → UUω
  where

  cons-zero-is-large-higher-directed-graph :
    is-large-higher-directed-graph β γ V 0

  cons-base-is-large-higher-directed-graph :
    Large-Relation β V → is-large-higher-directed-graph β γ V 1

  cons-ind-is-large-higher-directed-graph :
    (n : ℕ) →
    (E : Large-Relation β V) →
    ( {l1 l2 : Level} (u : V l1) (v : V l2) →
      is-higher-directed-graph-succ (γ l1 l2) n (E u v)) →
    is-large-higher-directed-graph β γ V (succ-ℕ (succ-ℕ n))

edge-is-large-higher-directed-graph :
  {α : Level → Level}
  (β γ : Level → Level → Level)
  (n : ℕ)
  (V : (l : Level) → UU (α l)) →
  is-large-higher-directed-graph β γ V (succ-ℕ n) →
  Large-Relation β V
edge-is-large-higher-directed-graph
  β γ .0 V (cons-base-is-large-higher-directed-graph E) =
  E
edge-is-large-higher-directed-graph
  β γ .(succ-ℕ n) V (cons-ind-is-large-higher-directed-graph n E _) =
  E

The large type of large higher directed graphs

record
  Large-Higher-Directed-Graph
    (α : Level → Level) (β γ : Level → Level → Level) (n : ℕ) : UUω
  where

  field
    vertex-Large-Higher-Directed-Graph : (l : Level) → UU (α l)

    is-higher-directed-graph-Large-Higher-Directed-Graph :
      is-large-higher-directed-graph β γ vertex-Large-Higher-Directed-Graph n

open Large-Higher-Directed-Graph public

edge-Large-Higher-Directed-Graph :
  {α : Level → Level} {β γ : Level → Level → Level} {n : ℕ}
  (G : Large-Higher-Directed-Graph α β γ (succ-ℕ n)) →
  Large-Relation β (vertex-Large-Higher-Directed-Graph G)
edge-Large-Higher-Directed-Graph {α} {β} {γ} {n} G =
  edge-is-large-higher-directed-graph β γ n
    ( vertex-Large-Higher-Directed-Graph G)
    ( is-higher-directed-graph-Large-Higher-Directed-Graph G)

Recent changes