# Directed graphs

```agda
module graph-theory.directed-graphs where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

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](foundation-core.equivalences.md), recall that
[$\Sigma$-types](foundation.dependent-pair-types.md) preserve equivalences and a
type family $A \to U$ is equivalent to $\sum_{(C : U)} C \to A$ by
[type duality](foundation.type-duality.md). Using these two observations we make
the following calculation:

$$
\begin{equation}
\begin{split}
\sum_{(V\,:\,\mathcal{U})} (V \to V \to \mathcal{U}) & \simeq \sum_{(V\,:\,\mathcal{U})}
 (V \times V \to \mathcal{U}) \\
 &\simeq \sum_{(V,E\,:\,\mathcal{U})} (E \to (V \times V)) \\
&\simeq  \sum_{(V,E\,:\,\mathcal{U})} ((E \to V) \times (E \to V))
\end{split}
\end{equation}
$$

## Definition

```agda
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)
  where

  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) →
    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

```agda
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)
    where

    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))
```

```agda
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))
```

## External links

- [Digraph](https://ncatlab.org/nlab/show/digraph) at $n$Lab
- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at $n$Lab
- [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikidata
- [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
- [Directed graph](https://mathworld.wolfram.com/DirectedGraph.html) at Wolfram
  Mathworld