The underlying trees of elements of W-types

module trees.underlying-trees-of-elements-of-w-types where
Imports
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.isolated-points
open import foundation.negation
open import foundation.propositions
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.combinator-directed-trees
open import trees.combinator-enriched-directed-trees
open import trees.directed-trees
open import trees.elementhood-relation-w-types
open import trees.enriched-directed-trees
open import trees.equivalences-directed-trees
open import trees.equivalences-enriched-directed-trees
open import trees.underlying-trees-elements-coalgebras-polynomial-endofunctors
open import trees.w-types

Idea

The underlying (enriched) directed tree of an element of a W-type is the underlying (enriched) directed tree of that element obtained via the coalgebra structure of 𝕎 A B.

Definitions

The underlying enriched directed tree of an element of a W-type

module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}
  where

  enriched-directed-tree-element-𝕎 :
    𝕎 A B  Enriched-Directed-Tree (l1  l2) (l1  l2) A B
  enriched-directed-tree-element-𝕎 =
    enriched-directed-tree-element-coalgebra (𝕎-Coalg A B)

The underlying graph of an element of a W-type

  graph-element-𝕎 : 𝕎 A B  Directed-Graph (l1  l2) (l1  l2)
  graph-element-𝕎 = graph-element-coalgebra (𝕎-Coalg A B)

  external-graph-element-𝕎 : 𝕎 A B  Directed-Graph (l1  l2) (l1  l2)
  external-graph-element-𝕎 = external-graph-element-coalgebra (𝕎-Coalg A B)

  node-external-graph-element-𝕎 : 𝕎 A B  UU (l1  l2)
  node-external-graph-element-𝕎 =
    node-external-graph-element-coalgebra (𝕎-Coalg A B)

  edge-external-graph-element-𝕎 :
    (w : 𝕎 A B) (x y : node-external-graph-element-𝕎 w)  UU (l1  l2)
  edge-external-graph-element-𝕎 =
    edge-external-graph-element-coalgebra (𝕎-Coalg A B)

  inclusion-graph-element-𝕎 :
    {u v : 𝕎 A B}  u ∈-𝕎 v 
    hom-Directed-Graph (graph-element-𝕎 u) (graph-element-𝕎 v)
  inclusion-graph-element-𝕎 = inclusion-element-coalgebra (𝕎-Coalg A B)

Nodes of the underlying directed tree of an element of a W-type

  node-element-𝕎 : 𝕎 A B  UU (l1  l2)
  node-element-𝕎 = node-element-coalgebra (𝕎-Coalg A B)

  node-inclusion-element-𝕎 :
    {u v : 𝕎 A B}  (u ∈-𝕎 v)  node-element-𝕎 u  node-element-𝕎 v
  node-inclusion-element-𝕎 = node-inclusion-element-coalgebra

The root of the underlying directed tree of an element of a W-type

  root-𝕎 : (w : 𝕎 A B)  node-element-𝕎 w
  root-𝕎 = root-coalgebra

  is-root-node-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w)  UU (l1  l2)
  is-root-node-element-𝕎 = is-root-element-coalgebra (𝕎-Coalg A B)

  is-isolated-root-element-𝕎 :
    (w : 𝕎 A B)  is-isolated (root-𝕎 w)
  is-isolated-root-element-𝕎 =
    is-isolated-root-element-coalgebra (𝕎-Coalg A B)

  is-contr-loop-space-root-graph-element-𝕎 :
    (w : 𝕎 A B)  is-contr (root-𝕎 w  root-𝕎 w)
  is-contr-loop-space-root-graph-element-𝕎 =
    is-contr-loop-space-root-element-coalgebra (𝕎-Coalg A B)

The edges of the underlying directed tree of an element of a W-type

  edge-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w)  UU (l1  l2)
  edge-element-𝕎 = edge-element-coalgebra (𝕎-Coalg A B)

  edge-to-root-element-𝕎 :
    {u v : 𝕎 A B} (H : u ∈-𝕎 v) 
    edge-element-𝕎 v
      ( node-inclusion-element-𝕎 H (root-𝕎 u))
      ( root-𝕎 v)
  edge-to-root-element-𝕎 = edge-to-root-element-coalgebra

  edge-inclusion-element-𝕎 :
    {u v : 𝕎 A B} (H : u ∈-𝕎 v) 
    {x y : node-element-𝕎 u} (e : edge-element-𝕎 u x y) 
    edge-element-𝕎 v
      ( node-inclusion-element-𝕎 H x)
      ( node-inclusion-element-𝕎 H y)
  edge-inclusion-element-𝕎 = edge-inclusion-element-coalgebra

  is-contr-edge-to-root-element-𝕎 :
    {u v : 𝕎 A B} (H : u ∈-𝕎 v) 
    is-contr
      ( edge-element-𝕎 v
        ( node-inclusion-element-𝕎 H (root-𝕎 u))
        ( root-𝕎 v))
  is-contr-edge-to-root-element-𝕎 =
    is-contr-edge-to-root-element-coalgebra (𝕎-Coalg A B)

  is-proof-irrelevant-edge-to-root-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    is-proof-irrelevant (edge-element-𝕎 w x (root-𝕎 w))
  is-proof-irrelevant-edge-to-root-element-𝕎 =
    is-proof-irrelevant-edge-to-root-element-coalgebra (𝕎-Coalg A B)

  is-prop-edge-to-root-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    is-prop (edge-element-𝕎 w x (root-𝕎 w))
  is-prop-edge-to-root-element-𝕎 =
    is-prop-edge-to-root-element-coalgebra (𝕎-Coalg A B)

  no-edge-from-root-graph-element-𝕎 :
    (w : 𝕎 A B) 
    is-empty (Σ (node-element-𝕎 w) (edge-element-𝕎 w (root-𝕎 w)))
  no-edge-from-root-graph-element-𝕎 =
    no-edge-from-root-element-coalgebra (𝕎-Coalg A B)

  is-empty-eq-root-node-inclusion-element-𝕎 :
    {v w : 𝕎 A B} (H : v ∈-𝕎 w) (x : node-element-𝕎 v) 
    ¬ (root-𝕎 w  node-inclusion-element-𝕎 H x)
  is-empty-eq-root-node-inclusion-element-𝕎 =
    is-empty-eq-root-node-inclusion-element-coalgebra (𝕎-Coalg A B)

The underlying directed tree of an element of a W-type

  directed-tree-element-𝕎 :
    𝕎 A B  Directed-Tree (l1  l2) (l1  l2)
  directed-tree-element-𝕎 =
    directed-tree-element-coalgebra (𝕎-Coalg A B)

  has-unique-predecessor-node-inclusion-element-𝕎 :
    {v w : 𝕎 A B} (H : v ∈-𝕎 w) (x : node-element-𝕎 v) 
    is-contr
      ( Σ ( node-element-𝕎 w)
          ( edge-element-𝕎 w (node-inclusion-element-𝕎 H x)))
  has-unique-predecessor-node-inclusion-element-𝕎 =
    has-unique-predecessor-node-inclusion-element-coalgebra (𝕎-Coalg A B)

  has-unique-predecessor-graph-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    is-contr
      ((root-𝕎 w  x) + Σ (node-element-𝕎 w) (edge-element-𝕎 w x))
  has-unique-predecessor-graph-element-𝕎 =
    has-unique-predecessor-element-coalgebra (𝕎-Coalg A B)

  walk-to-root-graph-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    walk-Directed-Graph (graph-element-𝕎 w) x (root-𝕎 w)
  walk-to-root-graph-element-𝕎 =
    walk-to-root-element-coalgebra (𝕎-Coalg A B)

  unique-walk-to-root-element-𝕎 :
    (w : 𝕎 A B)  is-tree-Directed-Graph' (graph-element-𝕎 w) (root-𝕎 w)
  unique-walk-to-root-element-𝕎 =
    unique-walk-to-root-element-coalgebra (𝕎-Coalg A B)

The underlying directed tree of an element of a W-type is enriched

module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}
  where

  shape-element-𝕎 :
    (w : 𝕎 A B)  node-element-𝕎 w  A
  shape-element-𝕎 =
    shape-element-coalgebra (𝕎-Coalg A B)

  map-enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    B (shape-element-𝕎 w x) 
    Σ (node-element-𝕎 w)  y  edge-element-𝕎 w y x)
  map-enrichment-element-𝕎 =
    map-enrichment-element-coalgebra (𝕎-Coalg A B)

  map-inv-enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    Σ (node-element-𝕎 w)  y  edge-element-𝕎 w y x) 
    B (shape-element-𝕎 w x)
  map-inv-enrichment-element-𝕎 =
    map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)

  issec-map-inv-enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    ( map-enrichment-element-𝕎 w x 
      map-inv-enrichment-element-𝕎 w x) ~ id
  issec-map-inv-enrichment-element-𝕎 =
    issec-map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)

  isretr-map-inv-enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    ( map-inv-enrichment-element-𝕎 w x 
      map-enrichment-element-𝕎 w x) ~ id
  isretr-map-inv-enrichment-element-𝕎 =
    isretr-map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)

  is-equiv-map-enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    is-equiv (map-enrichment-element-𝕎 w x)
  is-equiv-map-enrichment-element-𝕎 =
    is-equiv-map-enrichment-element-coalgebra (𝕎-Coalg A B)

  enrichment-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    B (shape-element-𝕎 w x) 
    Σ (node-element-𝕎 w)  y  edge-element-𝕎 w y x)
  enrichment-element-𝕎 =
    enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)

Properties

Characterization of equality of the type of nodes of the underlying graph of an element of 𝕎 A B

module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}
  where

  Eq-node-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w)  UU (l1  l2)
  Eq-node-element-𝕎 = Eq-node-element-coalgebra (𝕎-Coalg A B)

  root-refl-Eq-node-element-𝕎 :
    (w : 𝕎 A B)  Eq-node-element-𝕎 w (root-𝕎 w) (root-𝕎 w)
  root-refl-Eq-node-element-𝕎 w = root-refl-Eq-node-element-coalgebra

  node-inclusion-Eq-node-element-𝕎 :
    (w : 𝕎 A B) {u : 𝕎 A B} (H : u ∈-𝕎 w) {x y : node-element-𝕎 u} 
    Eq-node-element-𝕎 u x y 
    Eq-node-element-𝕎 w
      ( node-inclusion-element-𝕎 H x)
      ( node-inclusion-element-𝕎 H y)
  node-inclusion-Eq-node-element-𝕎 w =
    node-inclusion-Eq-node-element-coalgebra

  refl-Eq-node-element-𝕎 :
    {w : 𝕎 A B} (x : node-element-𝕎 w) 
    Eq-node-element-𝕎 w x x
  refl-Eq-node-element-𝕎 = refl-Eq-node-element-coalgebra (𝕎-Coalg A B)

  is-contr-total-Eq-node-element-𝕎 :
    (w : 𝕎 A B) (x : node-element-𝕎 w) 
    is-contr (Σ (node-element-𝕎 w) (Eq-node-element-𝕎 w x))
  is-contr-total-Eq-node-element-𝕎 =
    is-contr-total-Eq-node-element-coalgebra (𝕎-Coalg A B)

  Eq-eq-node-element-𝕎 :
    (w : 𝕎 A B) {x y : node-element-𝕎 w} 
    x  y  Eq-node-element-𝕎 w x y
  Eq-eq-node-element-𝕎 = Eq-eq-node-element-coalgebra (𝕎-Coalg A B)

  is-equiv-Eq-eq-node-element-𝕎 :
    (w : 𝕎 A B) (x y : node-element-𝕎 w) 
    is-equiv (Eq-eq-node-element-𝕎 w {x} {y})
  is-equiv-Eq-eq-node-element-𝕎 =
    is-equiv-Eq-eq-node-element-coalgebra (𝕎-Coalg A B)

  extensionality-node-element-𝕎 :
    (w : 𝕎 A B) (x y : node-element-𝕎 w) 
    (x  y)  Eq-node-element-𝕎 w x y
  extensionality-node-element-𝕎 =
    extensionality-node-element-coalgebra (𝕎-Coalg A B)

  eq-Eq-node-element-𝕎 :
    (w : 𝕎 A B) (x y : node-element-𝕎 w) 
    Eq-node-element-𝕎 w x y  x  y
  eq-Eq-node-element-𝕎 =
    eq-Eq-node-element-coalgebra (𝕎-Coalg A B)

The underlying tree of tree-𝕎 a α is the combinator tree of the underlying trees of α b indexed by b : B a

module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (w : 𝕎 A B)
  where

  node-compute-directed-tree-element-𝕎 :
    node-element-𝕎 w 
    node-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
  node-compute-directed-tree-element-𝕎 =
    node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  map-inv-node-compute-directed-tree-element-𝕎 :
    node-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b)) 
    node-element-𝕎 w
  map-inv-node-compute-directed-tree-element-𝕎 =
    map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  issec-map-inv-node-compute-directed-tree-element-𝕎 :
    ( node-compute-directed-tree-element-𝕎 
      map-inv-node-compute-directed-tree-element-𝕎) ~ id
  issec-map-inv-node-compute-directed-tree-element-𝕎 =
    issec-map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  isretr-map-inv-node-compute-directed-tree-element-𝕎 :
    ( map-inv-node-compute-directed-tree-element-𝕎 
      node-compute-directed-tree-element-𝕎) ~ id
  isretr-map-inv-node-compute-directed-tree-element-𝕎 =
    isretr-map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  is-equiv-node-compute-directed-tree-element-𝕎 :
    is-equiv node-compute-directed-tree-element-𝕎
  is-equiv-node-compute-directed-tree-element-𝕎 =
    is-equiv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  equiv-node-compute-directed-tree-element-𝕎 :
    node-element-𝕎 w 
    node-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
  equiv-node-compute-directed-tree-element-𝕎 =
    equiv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  edge-compute-directed-tree-element-𝕎 :
    (x y : node-element-𝕎 w) 
    edge-element-𝕎 w x y 
    edge-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
      ( node-compute-directed-tree-element-𝕎 x)
      ( node-compute-directed-tree-element-𝕎 y)
  edge-compute-directed-tree-element-𝕎 =
    edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  map-inv-edge-compute-directed-tree-element-𝕎 :
    ( x y : node-element-𝕎 w) 
    edge-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
      ( node-compute-directed-tree-element-𝕎 x)
      ( node-compute-directed-tree-element-𝕎 y) 
    edge-element-𝕎 w x y
  map-inv-edge-compute-directed-tree-element-𝕎 =
    map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  issec-map-inv-edge-compute-directed-tree-element-𝕎 :
    (x y : node-element-𝕎 w) 
    ( e :
      edge-combinator-Directed-Tree
        ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
        ( node-compute-directed-tree-element-𝕎 x)
        ( node-compute-directed-tree-element-𝕎 y)) 
    edge-compute-directed-tree-element-𝕎 x y
      ( map-inv-edge-compute-directed-tree-element-𝕎 x y e)  e
  issec-map-inv-edge-compute-directed-tree-element-𝕎 =
    issec-map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  isretr-map-inv-edge-compute-directed-tree-element-𝕎 :
    (x y : node-element-𝕎 w) (e : edge-element-𝕎 w x y) 
    map-inv-edge-compute-directed-tree-element-𝕎 x y
      ( edge-compute-directed-tree-element-𝕎 x y e)  e
  isretr-map-inv-edge-compute-directed-tree-element-𝕎 =
    isretr-map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  is-equiv-edge-compute-directed-tree-element-𝕎 :
    (x y : node-element-𝕎 w) 
    is-equiv (edge-compute-directed-tree-element-𝕎 x y)
  is-equiv-edge-compute-directed-tree-element-𝕎 =
    is-equiv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  equiv-edge-compute-directed-tree-element-𝕎 :
    (x y : node-element-𝕎 w) 
    edge-element-𝕎 w x y 
    edge-combinator-Directed-Tree
      ( λ b  directed-tree-element-𝕎 (component-𝕎 w b))
      ( node-compute-directed-tree-element-𝕎 x)
      ( node-compute-directed-tree-element-𝕎 y)
  equiv-edge-compute-directed-tree-element-𝕎 =
    equiv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  compute-directed-tree-element-𝕎 :
    equiv-Directed-Tree
      ( directed-tree-element-𝕎 w)
      ( combinator-Directed-Tree
        ( λ b  directed-tree-element-𝕎 (component-𝕎 w b)))
  compute-directed-tree-element-𝕎 =
    compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  shape-compute-enriched-directed-tree-element-𝕎 :
    shape-element-𝕎 w ~
    ( ( shape-combinator-Enriched-Directed-Tree A B
        ( λ b  enriched-directed-tree-element-𝕎 (component-𝕎 w b))) 
      ( node-compute-directed-tree-element-𝕎))
  shape-compute-enriched-directed-tree-element-𝕎 =
    shape-compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  enrichment-compute-enriched-directed-tree-element-𝕎 :
    (x : node-element-𝕎 w) 
    htpy-equiv
      ( ( equiv-direct-predecessor-equiv-Directed-Tree
          ( directed-tree-element-𝕎 w)
          ( combinator-Directed-Tree
            ( λ b  directed-tree-element-𝕎 (component-𝕎 w b)))
          ( compute-directed-tree-element-𝕎)
          ( x)) ∘e
        ( enrichment-element-𝕎 w x))
      ( ( enrichment-combinator-Enriched-Directed-Tree A B
          ( λ b  enriched-directed-tree-element-𝕎 (component-𝕎 w b))
          ( node-compute-directed-tree-element-𝕎 x)) ∘e
        ( equiv-tr B
          ( shape-compute-enriched-directed-tree-element-𝕎 x)))
  enrichment-compute-enriched-directed-tree-element-𝕎 =
    enrichment-compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w

  compute-enriched-directed-tree-element-𝕎 :
    equiv-Enriched-Directed-Tree A B
      ( enriched-directed-tree-element-𝕎 w)
      ( combinator-Enriched-Directed-Tree A B
        ( λ b  enriched-directed-tree-element-𝕎 (component-𝕎 w b)))
  compute-enriched-directed-tree-element-𝕎 =
    compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w