# Fibers of directed graphs

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-03.

module graph-theory.fibers-directed-graphs where

Imports
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.homotopies
open import foundation.identity-types
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

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

open import trees.directed-trees


## Idea

Consider a vertex x in a directed graph G. The fiber of G at x is a directed tree of which the type of nodes consists of vertices y equipped with a walk w from y to x, and the type of edges from (y , w) to (z , v) consist of an edge e : y → z such that w ＝ cons e v.

## Definitions

### The underlying graph of the fiber of G at x

module _
{l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G)
where

node-fiber-Directed-Graph : UU (l1 ⊔ l2)
node-fiber-Directed-Graph =
Σ (vertex-Directed-Graph G) (λ y → walk-Directed-Graph G y x)

module _
(u : node-fiber-Directed-Graph)
where

node-inclusion-fiber-Directed-Graph : vertex-Directed-Graph G
node-inclusion-fiber-Directed-Graph = pr1 u

walk-node-inclusion-fiber-Directed-Graph :
walk-Directed-Graph G node-inclusion-fiber-Directed-Graph x
walk-node-inclusion-fiber-Directed-Graph = pr2 u

root-fiber-Directed-Graph : node-fiber-Directed-Graph
pr1 root-fiber-Directed-Graph = x
pr2 root-fiber-Directed-Graph = refl-walk-Directed-Graph

is-root-fiber-Directed-Graph : node-fiber-Directed-Graph → UU (l1 ⊔ l2)
is-root-fiber-Directed-Graph y = root-fiber-Directed-Graph ＝ y

edge-fiber-Directed-Graph : (y z : node-fiber-Directed-Graph) → UU (l1 ⊔ l2)
edge-fiber-Directed-Graph y z =
Σ ( edge-Directed-Graph G
( node-inclusion-fiber-Directed-Graph y)
( node-inclusion-fiber-Directed-Graph z))
( λ e →
( walk-node-inclusion-fiber-Directed-Graph y) ＝
( cons-walk-Directed-Graph e
( walk-node-inclusion-fiber-Directed-Graph z)))

module _
(y z : node-fiber-Directed-Graph) (e : edge-fiber-Directed-Graph y z)
where

edge-inclusion-fiber-Directed-Graph :
edge-Directed-Graph G
( node-inclusion-fiber-Directed-Graph y)
( node-inclusion-fiber-Directed-Graph z)
edge-inclusion-fiber-Directed-Graph = pr1 e

walk-edge-fiber-Directed-Graph :
walk-node-inclusion-fiber-Directed-Graph y ＝
cons-walk-Directed-Graph
( edge-inclusion-fiber-Directed-Graph)
( walk-node-inclusion-fiber-Directed-Graph z)
walk-edge-fiber-Directed-Graph = pr2 e

graph-fiber-Directed-Graph : Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2)
pr1 graph-fiber-Directed-Graph = node-fiber-Directed-Graph
pr2 graph-fiber-Directed-Graph = edge-fiber-Directed-Graph

walk-fiber-Directed-Graph : (y z : node-fiber-Directed-Graph) → UU (l1 ⊔ l2)
walk-fiber-Directed-Graph = walk-Directed-Graph graph-fiber-Directed-Graph

walk-to-root-fiber-walk-Directed-Graph :
(y : vertex-Directed-Graph G) (w : walk-Directed-Graph G y x) →
walk-fiber-Directed-Graph (y , w) root-fiber-Directed-Graph
walk-to-root-fiber-walk-Directed-Graph y refl-walk-Directed-Graph =
refl-walk-Directed-Graph
walk-to-root-fiber-walk-Directed-Graph .y
( cons-walk-Directed-Graph {y} {z} e w) =
cons-walk-Directed-Graph
( e , refl)
( walk-to-root-fiber-walk-Directed-Graph z w)

walk-to-root-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph) →
walk-fiber-Directed-Graph y root-fiber-Directed-Graph
walk-to-root-fiber-Directed-Graph (y , w) =
walk-to-root-fiber-walk-Directed-Graph y w

inclusion-fiber-Directed-Graph :
hom-Directed-Graph graph-fiber-Directed-Graph G
pr1 inclusion-fiber-Directed-Graph = node-inclusion-fiber-Directed-Graph
pr2 inclusion-fiber-Directed-Graph = edge-inclusion-fiber-Directed-Graph


### The fiber of G at x as a directed tree

  center-unique-direct-successor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph) →
( is-root-fiber-Directed-Graph y) +
( Σ ( node-fiber-Directed-Graph) ( edge-fiber-Directed-Graph y))
center-unique-direct-successor-fiber-Directed-Graph
( y , refl-walk-Directed-Graph) =
inl refl
center-unique-direct-successor-fiber-Directed-Graph
( y , cons-walk-Directed-Graph {y} {z} e w) = inr ((z , w) , (e , refl))

contraction-unique-direct-successor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph) →
( p :
( is-root-fiber-Directed-Graph y) +
( Σ ( node-fiber-Directed-Graph) (edge-fiber-Directed-Graph y))) →
center-unique-direct-successor-fiber-Directed-Graph y ＝ p
contraction-unique-direct-successor-fiber-Directed-Graph ._ (inl refl) = refl
contraction-unique-direct-successor-fiber-Directed-Graph
( y , .(cons-walk-Directed-Graph e v)) (inr ((z , v) , e , refl)) =
refl

unique-direct-successor-fiber-Directed-Graph :
unique-direct-successor-Directed-Graph
( graph-fiber-Directed-Graph)
( root-fiber-Directed-Graph)
pr1 (unique-direct-successor-fiber-Directed-Graph y) =
center-unique-direct-successor-fiber-Directed-Graph y
pr2 (unique-direct-successor-fiber-Directed-Graph y) =
contraction-unique-direct-successor-fiber-Directed-Graph y

is-tree-fiber-Directed-Graph :
is-tree-Directed-Graph graph-fiber-Directed-Graph
is-tree-fiber-Directed-Graph =
is-tree-unique-direct-successor-Directed-Graph
graph-fiber-Directed-Graph
root-fiber-Directed-Graph
unique-direct-successor-fiber-Directed-Graph
walk-to-root-fiber-Directed-Graph

fiber-Directed-Graph : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2)
pr1 fiber-Directed-Graph = graph-fiber-Directed-Graph
pr2 fiber-Directed-Graph = is-tree-fiber-Directed-Graph


### Computing the direct predecessors of a node in a fiber

module _
{l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G)
where

direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) → UU (l1 ⊔ l2)
direct-predecessor-fiber-Directed-Graph =
direct-predecessor-Directed-Graph (graph-fiber-Directed-Graph G x)

direct-predecessor-inclusion-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
direct-predecessor-fiber-Directed-Graph y →
direct-predecessor-Directed-Graph G
( node-inclusion-fiber-Directed-Graph G x y)
direct-predecessor-inclusion-fiber-Directed-Graph =
direct-predecessor-hom-Directed-Graph
( graph-fiber-Directed-Graph G x)
( G)
( inclusion-fiber-Directed-Graph G x)

compute-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
direct-predecessor-fiber-Directed-Graph y ≃
direct-predecessor-Directed-Graph G
( node-inclusion-fiber-Directed-Graph G x y)
compute-direct-predecessor-fiber-Directed-Graph y =
( right-unit-law-Σ-is-contr (λ (u , e) → is-torsorial-Id' _)) ∘e
( interchange-Σ-Σ _)

map-compute-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
direct-predecessor-fiber-Directed-Graph y →
direct-predecessor-Directed-Graph G
( node-inclusion-fiber-Directed-Graph G x y)
map-compute-direct-predecessor-fiber-Directed-Graph y =
map-equiv (compute-direct-predecessor-fiber-Directed-Graph y)

htpy-compute-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
direct-predecessor-inclusion-fiber-Directed-Graph y ~
map-compute-direct-predecessor-fiber-Directed-Graph y
htpy-compute-direct-predecessor-fiber-Directed-Graph y t = refl

inv-compute-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
direct-predecessor-Directed-Graph G
( node-inclusion-fiber-Directed-Graph G x y) ≃
direct-predecessor-fiber-Directed-Graph y
inv-compute-direct-predecessor-fiber-Directed-Graph y =
inv-equiv (compute-direct-predecessor-fiber-Directed-Graph y)

Eq-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
(u v : direct-predecessor-fiber-Directed-Graph y) → UU (l1 ⊔ l2)
Eq-direct-predecessor-fiber-Directed-Graph y u v =
Σ ( pr1 (direct-predecessor-inclusion-fiber-Directed-Graph y u) ＝
pr1 (direct-predecessor-inclusion-fiber-Directed-Graph y v))
( λ p →
tr
( λ t →
edge-Directed-Graph G t (node-inclusion-fiber-Directed-Graph G x y))
( p)
( pr2 (direct-predecessor-inclusion-fiber-Directed-Graph y u)) ＝
pr2 (direct-predecessor-inclusion-fiber-Directed-Graph y v))

eq-Eq-direct-predecessor-fiber-Directed-Graph :
(y : node-fiber-Directed-Graph G x) →
( u v : direct-predecessor-fiber-Directed-Graph y) →
Eq-direct-predecessor-fiber-Directed-Graph y u v → u ＝ v
eq-Eq-direct-predecessor-fiber-Directed-Graph y u v p =
map-inv-equiv
( equiv-ap (compute-direct-predecessor-fiber-Directed-Graph y) u v)
( eq-pair-Σ' p)