# Equivalences of directed graphs

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

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.transposition-identifications-along-equivalences
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.morphisms-directed-graphs
```

</details>

## Idea

An **equivalence of directed graphs** from a
[directed graph](graph-theory.directed-graphs.md) `(V,E)` to a directed graph
`(V',E')` consists of an [equivalence](foundation-core.equivalences.md)
`e : V ≃ V'` of vertices, and a family of equivalences `E x y ≃ E' (e x) (e y)`
of edges indexed by `x y : V`.

## Definitions

### Equivalences of directed graphs

```agda
equiv-Directed-Graph :
  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
equiv-Directed-Graph G H =
  Σ ( vertex-Directed-Graph G ≃ vertex-Directed-Graph H)
    ( λ e →
      (x y : vertex-Directed-Graph G) →
      edge-Directed-Graph G x y ≃
      edge-Directed-Graph H (map-equiv e x) (map-equiv e y))

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

  equiv-vertex-equiv-Directed-Graph :
    vertex-Directed-Graph G ≃ vertex-Directed-Graph H
  equiv-vertex-equiv-Directed-Graph = pr1 e

  vertex-equiv-Directed-Graph :
    vertex-Directed-Graph G → vertex-Directed-Graph H
  vertex-equiv-Directed-Graph = map-equiv equiv-vertex-equiv-Directed-Graph

  is-equiv-vertex-equiv-Directed-Graph :
    is-equiv vertex-equiv-Directed-Graph
  is-equiv-vertex-equiv-Directed-Graph =
    is-equiv-map-equiv equiv-vertex-equiv-Directed-Graph

  inv-vertex-equiv-Directed-Graph :
    vertex-Directed-Graph H → vertex-Directed-Graph G
  inv-vertex-equiv-Directed-Graph =
    map-inv-equiv equiv-vertex-equiv-Directed-Graph

  is-section-inv-vertex-equiv-Directed-Graph :
    ( vertex-equiv-Directed-Graph ∘ inv-vertex-equiv-Directed-Graph) ~ id
  is-section-inv-vertex-equiv-Directed-Graph =
    is-section-map-inv-equiv equiv-vertex-equiv-Directed-Graph

  is-retraction-inv-vertex-equiv-Directed-Graph :
    ( inv-vertex-equiv-Directed-Graph ∘ vertex-equiv-Directed-Graph) ~ id
  is-retraction-inv-vertex-equiv-Directed-Graph =
    is-retraction-map-inv-equiv equiv-vertex-equiv-Directed-Graph

  equiv-edge-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph G) →
    edge-Directed-Graph G x y ≃
    edge-Directed-Graph H
      ( vertex-equiv-Directed-Graph x)
      ( vertex-equiv-Directed-Graph y)
  equiv-edge-equiv-Directed-Graph = pr2 e

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

  is-equiv-edge-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph G) → is-equiv (edge-equiv-Directed-Graph x y)
  is-equiv-edge-equiv-Directed-Graph x y =
    is-equiv-map-equiv (equiv-edge-equiv-Directed-Graph x y)
```

### The condition on a morphism of directed graphs to be an equivalence

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

  is-equiv-hom-Directed-Graph :
    hom-Directed-Graph G H → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-equiv-hom-Directed-Graph f =
    ( is-equiv (vertex-hom-Directed-Graph G H f)) ×
    ( (x y : vertex-Directed-Graph G) →
      is-equiv (edge-hom-Directed-Graph G H f {x} {y}))

  equiv-is-equiv-hom-Directed-Graph :
    (f : hom-Directed-Graph G H) →
    is-equiv-hom-Directed-Graph f → equiv-Directed-Graph G H
  pr1 (equiv-is-equiv-hom-Directed-Graph f (K , L)) =
    ( vertex-hom-Directed-Graph G H f , K)
  pr2 (equiv-is-equiv-hom-Directed-Graph f (K , L)) x y =
    ( edge-hom-Directed-Graph G H f , L x y)

  compute-equiv-Directed-Graph :
    equiv-Directed-Graph G H ≃
    Σ (hom-Directed-Graph G H) is-equiv-hom-Directed-Graph
  compute-equiv-Directed-Graph =
    interchange-Σ-Σ
      ( λ fV H fE → (x y : vertex-Directed-Graph G) → is-equiv (fE x y)) ∘e
      ( equiv-tot
        ( λ fV →
          distributive-Π-Σ ∘e equiv-Π-equiv-family (λ x → distributive-Π-Σ)))

  hom-equiv-Directed-Graph :
    equiv-Directed-Graph G H → hom-Directed-Graph G H
  hom-equiv-Directed-Graph e =
    pr1 (map-equiv compute-equiv-Directed-Graph e)

  compute-hom-equiv-Directed-Graph :
    (e : equiv-Directed-Graph G H) →
    hom-equiv-Directed-Graph e ＝
    ( vertex-equiv-Directed-Graph G H e , edge-equiv-Directed-Graph G H e)
  compute-hom-equiv-Directed-Graph e = refl

  is-equiv-equiv-Directed-Graph :
    (e : equiv-Directed-Graph G H) →
    is-equiv-hom-Directed-Graph (hom-equiv-Directed-Graph e)
  is-equiv-equiv-Directed-Graph e =
    pr2 (map-equiv compute-equiv-Directed-Graph e)
```

### Identity equivalences of directed graphs

```agda
id-equiv-Directed-Graph :
  {l1 l2 : Level} (G : Directed-Graph l1 l2) → equiv-Directed-Graph G G
pr1 (id-equiv-Directed-Graph G) = id-equiv
pr2 (id-equiv-Directed-Graph G) x y = id-equiv
```

### Composition of equivalences of directed graphs

```agda
module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
  (K : Directed-Graph l5 l6)
  (g : equiv-Directed-Graph H K) (f : equiv-Directed-Graph G H)
  where

  equiv-vertex-comp-equiv-Directed-Graph :
    vertex-Directed-Graph G ≃ vertex-Directed-Graph K
  equiv-vertex-comp-equiv-Directed-Graph =
    ( equiv-vertex-equiv-Directed-Graph H K g) ∘e
    ( equiv-vertex-equiv-Directed-Graph G H f)

  vertex-comp-equiv-Directed-Graph :
    vertex-Directed-Graph G → vertex-Directed-Graph K
  vertex-comp-equiv-Directed-Graph =
    map-equiv equiv-vertex-comp-equiv-Directed-Graph

  equiv-edge-comp-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph G) →
    edge-Directed-Graph G x y ≃
    edge-Directed-Graph K
      ( vertex-comp-equiv-Directed-Graph x)
      ( vertex-comp-equiv-Directed-Graph y)
  equiv-edge-comp-equiv-Directed-Graph x y =
    ( equiv-edge-equiv-Directed-Graph H K g
      ( vertex-equiv-Directed-Graph G H f x)
      ( vertex-equiv-Directed-Graph G H f y)) ∘e
    ( equiv-edge-equiv-Directed-Graph G H f x y)

  edge-comp-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph G) →
    edge-Directed-Graph G x y →
    edge-Directed-Graph K
      ( vertex-comp-equiv-Directed-Graph x)
      ( vertex-comp-equiv-Directed-Graph y)
  edge-comp-equiv-Directed-Graph x y =
    map-equiv (equiv-edge-comp-equiv-Directed-Graph x y)

  comp-equiv-Directed-Graph :
    equiv-Directed-Graph G K
  pr1 comp-equiv-Directed-Graph =
    equiv-vertex-comp-equiv-Directed-Graph
  pr2 comp-equiv-Directed-Graph =
    equiv-edge-comp-equiv-Directed-Graph
```

### Homotopies of equivalences of directed graphs

```agda
htpy-equiv-Directed-Graph :
  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
  (e f : equiv-Directed-Graph G H) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
htpy-equiv-Directed-Graph G H e f =
  htpy-hom-Directed-Graph G H
    ( hom-equiv-Directed-Graph G H e)
    ( hom-equiv-Directed-Graph G H f)
```

### The reflexivity homotopy of equivalences of directed graphs

```agda
refl-htpy-equiv-Directed-Graph :
  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
  (e : equiv-Directed-Graph G H) → htpy-equiv-Directed-Graph G H e e
refl-htpy-equiv-Directed-Graph G H e =
  refl-htpy-hom-Directed-Graph G H (hom-equiv-Directed-Graph G H e)
```

## Properties

### Homotopies characterize identifications of equivalences of directed graphs

```agda
module _
  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
  (e : equiv-Directed-Graph G H)
  where

  is-torsorial-htpy-equiv-Directed-Graph :
    is-torsorial (htpy-equiv-Directed-Graph G H e)
  is-torsorial-htpy-equiv-Directed-Graph =
    is-torsorial-Eq-structure
      ( is-torsorial-htpy-equiv (equiv-vertex-equiv-Directed-Graph G H e))
      ( equiv-vertex-equiv-Directed-Graph G H e , refl-htpy)
      ( is-torsorial-Eq-Π
        ( λ x →
          is-torsorial-Eq-Π
            ( λ y →
              is-torsorial-htpy-equiv
                ( equiv-edge-equiv-Directed-Graph G H e x y))))

  htpy-eq-equiv-Directed-Graph :
    (f : equiv-Directed-Graph G H) → e ＝ f → htpy-equiv-Directed-Graph G H e f
  htpy-eq-equiv-Directed-Graph .e refl = refl-htpy-equiv-Directed-Graph G H e

  is-equiv-htpy-eq-equiv-Directed-Graph :
    (f : equiv-Directed-Graph G H) →
    is-equiv (htpy-eq-equiv-Directed-Graph f)
  is-equiv-htpy-eq-equiv-Directed-Graph =
    fundamental-theorem-id
      is-torsorial-htpy-equiv-Directed-Graph
      htpy-eq-equiv-Directed-Graph

  extensionality-equiv-Directed-Graph :
    (f : equiv-Directed-Graph G H) →
    (e ＝ f) ≃ htpy-equiv-Directed-Graph G H e f
  pr1 (extensionality-equiv-Directed-Graph f) = htpy-eq-equiv-Directed-Graph f
  pr2 (extensionality-equiv-Directed-Graph f) =
    is-equiv-htpy-eq-equiv-Directed-Graph f

  eq-htpy-equiv-Directed-Graph :
    (f : equiv-Directed-Graph G H) →
    htpy-equiv-Directed-Graph G H e f → e ＝ f
  eq-htpy-equiv-Directed-Graph f =
    map-inv-equiv (extensionality-equiv-Directed-Graph f)
```

### Equivalences of directed graphs characterize identifications of directed graphs

```agda
module _
  {l1 l2 : Level} (G : Directed-Graph l1 l2)
  where

  extensionality-Directed-Graph :
    (H : Directed-Graph l1 l2) → (G ＝ H) ≃ equiv-Directed-Graph G H
  extensionality-Directed-Graph =
    extensionality-Σ
      ( λ {V} E e →
        ( x y : vertex-Directed-Graph G) →
        edge-Directed-Graph G x y ≃ E (map-equiv e x) (map-equiv e y))
      ( id-equiv)
      ( λ x y → id-equiv)
      ( λ X → equiv-univalence)
      ( extensionality-Π
          ( λ x y → edge-Directed-Graph G x y)
          ( λ x F →
            (y : vertex-Directed-Graph G) → edge-Directed-Graph G x y ≃ F y)
          ( λ x →
            extensionality-Π
              ( λ y → edge-Directed-Graph G x y)
              ( λ y X → edge-Directed-Graph G x y ≃ X)
              ( λ y X → equiv-univalence)))

  equiv-eq-Directed-Graph :
    (H : Directed-Graph l1 l2) → (G ＝ H) → equiv-Directed-Graph G H
  equiv-eq-Directed-Graph H = map-equiv (extensionality-Directed-Graph H)

  eq-equiv-Directed-Graph :
    (H : Directed-Graph l1 l2) → equiv-Directed-Graph G H → (G ＝ H)
  eq-equiv-Directed-Graph H = map-inv-equiv (extensionality-Directed-Graph H)

  is-torsorial-equiv-Directed-Graph :
    is-torsorial (equiv-Directed-Graph G)
  is-torsorial-equiv-Directed-Graph =
    is-contr-equiv'
      ( Σ (Directed-Graph l1 l2) (λ H → G ＝ H))
      ( equiv-tot extensionality-Directed-Graph)
      ( is-torsorial-Id G)
```

### The inverse of an equivalence of directed trees

```agda
module _
  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
  (f : equiv-Directed-Graph G H)
  where

  equiv-vertex-inv-equiv-Directed-Graph :
    vertex-Directed-Graph H ≃ vertex-Directed-Graph G
  equiv-vertex-inv-equiv-Directed-Graph =
    inv-equiv (equiv-vertex-equiv-Directed-Graph G H f)

  vertex-inv-equiv-Directed-Graph :
    vertex-Directed-Graph H → vertex-Directed-Graph G
  vertex-inv-equiv-Directed-Graph =
    map-inv-equiv (equiv-vertex-equiv-Directed-Graph G H f)

  is-section-vertex-inv-equiv-Directed-Graph :
    ( vertex-equiv-Directed-Graph G H f ∘
      vertex-inv-equiv-Directed-Graph) ~ id
  is-section-vertex-inv-equiv-Directed-Graph =
    is-section-map-inv-equiv (equiv-vertex-equiv-Directed-Graph G H f)

  is-retraction-vertex-inv-equiv-Directed-Graph :
    ( vertex-inv-equiv-Directed-Graph ∘
      vertex-equiv-Directed-Graph G H f) ~ id
  is-retraction-vertex-inv-equiv-Directed-Graph =
    is-retraction-map-inv-equiv (equiv-vertex-equiv-Directed-Graph G H f)

  is-equiv-vertex-inv-equiv-Directed-Graph :
    is-equiv vertex-inv-equiv-Directed-Graph
  is-equiv-vertex-inv-equiv-Directed-Graph =
    is-equiv-map-inv-equiv (equiv-vertex-equiv-Directed-Graph G H f)

  equiv-edge-inv-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph H) →
    edge-Directed-Graph H x y ≃
    edge-Directed-Graph G
      ( vertex-inv-equiv-Directed-Graph x)
      ( vertex-inv-equiv-Directed-Graph y)
  equiv-edge-inv-equiv-Directed-Graph x y =
    ( inv-equiv
      ( equiv-edge-equiv-Directed-Graph G H f
        ( vertex-inv-equiv-Directed-Graph x)
        ( vertex-inv-equiv-Directed-Graph y))) ∘e
    ( equiv-binary-tr
      ( edge-Directed-Graph H)
      ( inv (is-section-vertex-inv-equiv-Directed-Graph x))
      ( inv (is-section-vertex-inv-equiv-Directed-Graph y)))

  edge-inv-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph H) →
    edge-Directed-Graph H x y →
    edge-Directed-Graph G
      ( vertex-inv-equiv-Directed-Graph x)
      ( vertex-inv-equiv-Directed-Graph y)
  edge-inv-equiv-Directed-Graph x y =
    map-equiv (equiv-edge-inv-equiv-Directed-Graph x y)

  hom-inv-equiv-Directed-Graph : hom-Directed-Graph H G
  pr1 hom-inv-equiv-Directed-Graph = vertex-inv-equiv-Directed-Graph
  pr2 hom-inv-equiv-Directed-Graph = edge-inv-equiv-Directed-Graph

  inv-equiv-Directed-Graph : equiv-Directed-Graph H G
  pr1 inv-equiv-Directed-Graph = equiv-vertex-inv-equiv-Directed-Graph
  pr2 inv-equiv-Directed-Graph = equiv-edge-inv-equiv-Directed-Graph

  vertex-is-section-inv-equiv-Directed-Graph :
    ( vertex-equiv-Directed-Graph G H f ∘ vertex-inv-equiv-Directed-Graph) ~ id
  vertex-is-section-inv-equiv-Directed-Graph =
    is-section-vertex-inv-equiv-Directed-Graph

  edge-is-section-inv-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph H) (e : edge-Directed-Graph H x y) →
    binary-tr
      ( edge-Directed-Graph H)
      ( vertex-is-section-inv-equiv-Directed-Graph x)
      ( vertex-is-section-inv-equiv-Directed-Graph y)
      ( edge-equiv-Directed-Graph G H f
        ( vertex-inv-equiv-Directed-Graph x)
        ( vertex-inv-equiv-Directed-Graph y)
        ( edge-inv-equiv-Directed-Graph x y e)) ＝ e
  edge-is-section-inv-equiv-Directed-Graph x y e =
    ( ap
      ( binary-tr
        ( edge-Directed-Graph H)
        ( vertex-is-section-inv-equiv-Directed-Graph x)
        ( vertex-is-section-inv-equiv-Directed-Graph y))
        ( is-section-map-inv-equiv
          ( equiv-edge-equiv-Directed-Graph G H f
            ( vertex-inv-equiv-Directed-Graph x)
            ( vertex-inv-equiv-Directed-Graph y))
          ( binary-tr
            ( edge-Directed-Graph H)
            ( inv (is-section-map-inv-equiv (pr1 f) x))
            ( inv (is-section-map-inv-equiv (pr1 f) y))
            ( e)))) ∙
    ( ( inv
        ( binary-tr-concat
          ( edge-Directed-Graph H)
          ( inv (vertex-is-section-inv-equiv-Directed-Graph x))
          ( vertex-is-section-inv-equiv-Directed-Graph x)
          ( inv (vertex-is-section-inv-equiv-Directed-Graph y))
          ( vertex-is-section-inv-equiv-Directed-Graph y)
          ( e))) ∙
      ( ap-binary
        ( λ p q → binary-tr (edge-Directed-Graph H) p q e)
        ( left-inv (vertex-is-section-inv-equiv-Directed-Graph x))
        ( left-inv (vertex-is-section-inv-equiv-Directed-Graph y))))

  is-section-inv-equiv-Directed-Graph :
    htpy-equiv-Directed-Graph H H
      ( comp-equiv-Directed-Graph H G H f (inv-equiv-Directed-Graph))
      ( id-equiv-Directed-Graph H)
  pr1 is-section-inv-equiv-Directed-Graph =
    vertex-is-section-inv-equiv-Directed-Graph
  pr2 is-section-inv-equiv-Directed-Graph =
    edge-is-section-inv-equiv-Directed-Graph

  vertex-is-retraction-inv-equiv-Directed-Graph :
    ( vertex-inv-equiv-Directed-Graph ∘ vertex-equiv-Directed-Graph G H f) ~ id
  vertex-is-retraction-inv-equiv-Directed-Graph =
    is-retraction-vertex-inv-equiv-Directed-Graph

  edge-is-retraction-inv-equiv-Directed-Graph :
    (x y : vertex-Directed-Graph G) (e : edge-Directed-Graph G x y) →
    binary-tr
      ( edge-Directed-Graph G)
      ( vertex-is-retraction-inv-equiv-Directed-Graph x)
      ( vertex-is-retraction-inv-equiv-Directed-Graph y)
      ( edge-inv-equiv-Directed-Graph
        ( vertex-equiv-Directed-Graph G H f x)
        ( vertex-equiv-Directed-Graph G H f y)
        ( edge-equiv-Directed-Graph G H f x y e)) ＝ e
  edge-is-retraction-inv-equiv-Directed-Graph x y e =
    transpose-binary-path-over'
      ( edge-Directed-Graph G)
      ( vertex-is-retraction-inv-equiv-Directed-Graph x)
      ( vertex-is-retraction-inv-equiv-Directed-Graph y)
      ( map-eq-transpose-equiv-inv
        ( equiv-edge-equiv-Directed-Graph G H f
          ( vertex-inv-equiv-Directed-Graph
            ( vertex-equiv-Directed-Graph G H f x))
          ( vertex-inv-equiv-Directed-Graph
            ( vertex-equiv-Directed-Graph G H f y)))
        ( ( ap-binary
            ( λ u v →
              binary-tr
                ( edge-Directed-Graph H)
                ( u)
                ( v)
                ( edge-equiv-Directed-Graph G H f x y e))
            ( ( ap
                ( inv)
                ( coherence-map-inv-equiv
                  ( equiv-vertex-equiv-Directed-Graph G H f)
                  ( x))) ∙
              ( inv
                ( ap-inv
                  ( vertex-equiv-Directed-Graph G H f)
                  ( vertex-is-retraction-inv-equiv-Directed-Graph x))))
            ( ( ap
                ( inv)
                ( coherence-map-inv-equiv
                  ( equiv-vertex-equiv-Directed-Graph G H f)
                  ( y))) ∙
              ( inv
                ( ap-inv
                  ( vertex-equiv-Directed-Graph G H f)
                  ( vertex-is-retraction-inv-equiv-Directed-Graph y))))) ∙
          ( binary-tr-ap
            ( edge-Directed-Graph H)
            ( edge-equiv-Directed-Graph G H f)
            ( inv (vertex-is-retraction-inv-equiv-Directed-Graph x))
            ( inv (vertex-is-retraction-inv-equiv-Directed-Graph y))
            ( refl))))

  is-retraction-inv-equiv-Directed-Graph :
    htpy-equiv-Directed-Graph G G
      ( comp-equiv-Directed-Graph G H G (inv-equiv-Directed-Graph) f)
      ( id-equiv-Directed-Graph G)
  pr1 is-retraction-inv-equiv-Directed-Graph =
    vertex-is-retraction-inv-equiv-Directed-Graph
  pr2 is-retraction-inv-equiv-Directed-Graph =
    edge-is-retraction-inv-equiv-Directed-Graph
```

## External links

- [Graph isomoprhism](https://www.wikidata.org/entity/Q303100) at Wikidata
- [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
  Wikipedia
- [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
  Wolfram Mathworld
- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab