# Higher directed graphs

Content created by Fredrik Bakke.

Created on 2024-03-24.

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

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

open import graph-theory.directed-graphs

## Idea

A directed -graph consists of a type of vertices equipped with a binary family of directed n-1-graphs on its edges, where a directed 0-graph consists of just a type of vertices.

## Definition

### The structure of a higher directed graph on a type of vertices

is-higher-directed-graph-succ :
{l1 : Level} (l2 : Level) (n : )  UU l1  UU (l1  lsuc l2)
is-higher-directed-graph-succ l2 zero-ℕ V =
Relation l2 V
is-higher-directed-graph-succ l2 (succ-ℕ n) V =
Σ ( is-higher-directed-graph-succ l2 0 V)
( λ E  (u v : V)  is-higher-directed-graph-succ l2 n (E u v))

edge-is-higher-directed-graph-succ :
{l1 l2 : Level} {n : } (V : UU l1)
is-higher-directed-graph-succ l2 n V  Relation l2 V
edge-is-higher-directed-graph-succ {n = zero-ℕ} V E = E
edge-is-higher-directed-graph-succ {n = succ-ℕ n} V (E , _) = E

### The type of higher directed graphs

Higher-Directed-Graph : (l : Level) (n : )  UU (lsuc l)
Higher-Directed-Graph l 0 = UU l
Higher-Directed-Graph l (succ-ℕ n) =
Σ (UU l)  V  V  V  Higher-Directed-Graph l n)

vertex-Higher-Directed-Graph :
{n : } {l : Level}  Higher-Directed-Graph l n  UU l
vertex-Higher-Directed-Graph {0} G = G
vertex-Higher-Directed-Graph {succ-ℕ n} = pr1

edge-Higher-Directed-Graph :
{n : } {l : Level} (G : Higher-Directed-Graph l (succ-ℕ n))
vertex-Higher-Directed-Graph G  vertex-Higher-Directed-Graph G  UU l
edge-Higher-Directed-Graph {0} = pr2
edge-Higher-Directed-Graph {succ-ℕ n} G x y = pr1 (pr2 G x y)

## Properties

### Directed 1-graphs are just directed graphs

eq-Directed-Graph-Higher-Directed-Graph-1 :
{l : Level}  Higher-Directed-Graph l 1  Directed-Graph l l
eq-Directed-Graph-Higher-Directed-Graph-1 = refl