# Equivalences of directed graphs

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Vojtěch Štěpančík.

Created on 2023-01-29.

module graph-theory.equivalences-directed-graphs where

Imports
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


## Idea

An equivalence of directed graphs from a directed graph (V,E) to a directed graph (V',E') consists of an equivalence 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

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

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

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

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

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

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

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

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

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