Enriched directed trees

module trees.enriched-directed-trees where

open import elementary-number-theory.natural-numbers

open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
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 trees.directed-trees

Idea

Consider a type A and a type family B over A. An (A,B)-enriched directed tree is a directed tree T equipped with a map

  shape : node-Directed-Tree T → A

and for each node x an equivalence

  e : B (shape x) ≃ Σ (node-Directed-Tree T) (λ y → edge-Directed-Tree T y x)

By this equivalence, there is a higher group action of Ω (A , f x) on the type of children of x.

Definition

Enriched-Directed-Tree :
  {l1 l2 : Level} (l3 l4 : Level) (A : UU l1) (B : A → UU l2) →
  UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
Enriched-Directed-Tree l3 l4 A B =
  Σ ( Directed-Tree l3 l4)
    ( λ T →
      Σ ( node-Directed-Tree T → A)
        ( λ f →
          (x : node-Directed-Tree T) →
          B (f x) ≃
          Σ (node-Directed-Tree T) (λ y → edge-Directed-Tree T y x)))

module _
  {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2)
  (T : Enriched-Directed-Tree l3 l4 A B)
  where

  directed-tree-Enriched-Directed-Tree : Directed-Tree l3 l4
  directed-tree-Enriched-Directed-Tree = pr1 T

  graph-Enriched-Directed-Tree : Directed-Graph l3 l4
  graph-Enriched-Directed-Tree =
    graph-Directed-Tree directed-tree-Enriched-Directed-Tree

  node-Enriched-Directed-Tree : UU l3
  node-Enriched-Directed-Tree =
    node-Directed-Tree directed-tree-Enriched-Directed-Tree

  edge-Enriched-Directed-Tree :
    (x y : node-Enriched-Directed-Tree) → UU l4
  edge-Enriched-Directed-Tree =
    edge-Directed-Tree directed-tree-Enriched-Directed-Tree

  direct-predecessor-Enriched-Directed-Tree :
    node-Enriched-Directed-Tree → UU (l3 ⊔ l4)
  direct-predecessor-Enriched-Directed-Tree =
    direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree

  node-direct-predecessor-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    direct-predecessor-Enriched-Directed-Tree x → node-Enriched-Directed-Tree
  node-direct-predecessor-Enriched-Directed-Tree =
    node-direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree

  edge-direct-predecessor-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree)
    (y : direct-predecessor-Enriched-Directed-Tree x) →
    edge-Enriched-Directed-Tree
      ( node-direct-predecessor-Enriched-Directed-Tree x y)
      ( x)
  edge-direct-predecessor-Enriched-Directed-Tree =
    edge-direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree

  walk-Enriched-Directed-Tree :
    (x y : node-Enriched-Directed-Tree) → UU (l3 ⊔ l4)
  walk-Enriched-Directed-Tree =
    walk-Directed-Tree directed-tree-Enriched-Directed-Tree

  refl-walk-Enriched-Directed-Tree :
    {x : node-Enriched-Directed-Tree} → walk-Enriched-Directed-Tree x x
  refl-walk-Enriched-Directed-Tree =
    refl-walk-Directed-Tree directed-tree-Enriched-Directed-Tree

  cons-walk-Enriched-Directed-Tree :
    {x y z : node-Enriched-Directed-Tree} → edge-Enriched-Directed-Tree x y →
    walk-Enriched-Directed-Tree y z → walk-Enriched-Directed-Tree x z
  cons-walk-Enriched-Directed-Tree =
    cons-walk-Directed-Tree directed-tree-Enriched-Directed-Tree

  unit-walk-Enriched-Directed-Tree :
    {x y : node-Enriched-Directed-Tree} →
    edge-Enriched-Directed-Tree x y → walk-Enriched-Directed-Tree x y
  unit-walk-Enriched-Directed-Tree =
    unit-walk-Directed-Tree directed-tree-Enriched-Directed-Tree

  length-walk-Enriched-Directed-Tree :
    {x y : node-Enriched-Directed-Tree} →
    walk-Enriched-Directed-Tree x y → ℕ
  length-walk-Enriched-Directed-Tree =
    length-walk-Directed-Tree directed-tree-Enriched-Directed-Tree

  root-Enriched-Directed-Tree : node-Enriched-Directed-Tree
  root-Enriched-Directed-Tree =
    root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-root-Enriched-Directed-Tree :
    node-Enriched-Directed-Tree → UU l3
  is-root-Enriched-Directed-Tree =
    is-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-isolated-root-Enriched-Directed-Tree :
    is-isolated root-Enriched-Directed-Tree
  is-isolated-root-Enriched-Directed-Tree =
    is-isolated-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-prop-is-root-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-prop (is-root-Enriched-Directed-Tree x)
  is-prop-is-root-Enriched-Directed-Tree =
    is-prop-is-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-root-enriched-directed-tree-Prop :
    (x : node-Enriched-Directed-Tree) → Prop l3
  is-root-enriched-directed-tree-Prop =
    is-root-directed-tree-Prop directed-tree-Enriched-Directed-Tree

  is-contr-loop-space-root-Enriched-Directed-Tree :
    is-contr (root-Enriched-Directed-Tree ＝ root-Enriched-Directed-Tree)
  is-contr-loop-space-root-Enriched-Directed-Tree =
    is-contr-loop-space-root-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  is-proper-node-Enriched-Directed-Tree :
    node-Enriched-Directed-Tree → UU l3
  is-proper-node-Enriched-Directed-Tree =
    is-proper-node-Directed-Tree directed-tree-Enriched-Directed-Tree

  eq-refl-root-Enriched-Directed-Tree :
    (p : root-Enriched-Directed-Tree ＝ root-Enriched-Directed-Tree) → p ＝ refl
  eq-refl-root-Enriched-Directed-Tree =
    eq-refl-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  eq-refl-root-Enriched-Directed-Tree' :
    (p : root-Enriched-Directed-Tree ＝ root-Enriched-Directed-Tree) → refl ＝ p
  eq-refl-root-Enriched-Directed-Tree' =
    eq-refl-root-Directed-Tree' directed-tree-Enriched-Directed-Tree

  no-direct-successor-root-Enriched-Directed-Tree :
    ¬ ( Σ ( node-Enriched-Directed-Tree)
          ( edge-Enriched-Directed-Tree root-Enriched-Directed-Tree))
  no-direct-successor-root-Enriched-Directed-Tree =
    no-direct-successor-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-proper-node-direct-successor-Enriched-Directed-Tree :
    {x y : node-Enriched-Directed-Tree} (e : edge-Enriched-Directed-Tree x y) →
    ¬ (is-root-Enriched-Directed-Tree x)
  is-proper-node-direct-successor-Enriched-Directed-Tree =
    is-proper-node-direct-successor-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  is-proof-irrelevant-edge-to-root-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-proof-irrelevant
      ( edge-Enriched-Directed-Tree x root-Enriched-Directed-Tree)
  is-proof-irrelevant-edge-to-root-Enriched-Directed-Tree =
    is-proof-irrelevant-edge-to-root-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  is-prop-edge-to-root-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-prop (edge-Enriched-Directed-Tree x root-Enriched-Directed-Tree)
  is-prop-edge-to-root-Enriched-Directed-Tree =
    is-prop-edge-to-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  is-tree-Enriched-Directed-Tree :
    is-tree-Directed-Graph graph-Enriched-Directed-Tree
  is-tree-Enriched-Directed-Tree =
    is-tree-Directed-Tree directed-tree-Enriched-Directed-Tree

  unique-walk-to-root-Enriched-Directed-Tree :
    is-tree-Directed-Graph'
      graph-Enriched-Directed-Tree
      root-Enriched-Directed-Tree
  unique-walk-to-root-Enriched-Directed-Tree =
    unique-walk-to-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  uniqueness-root-Enriched-Directed-Tree :
    (H : is-tree-Directed-Graph graph-Enriched-Directed-Tree) →
    is-root-Enriched-Directed-Tree (pr1 H)
  uniqueness-root-Enriched-Directed-Tree =
    uniqueness-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  walk-to-root-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    walk-Enriched-Directed-Tree x root-Enriched-Directed-Tree
  walk-to-root-Enriched-Directed-Tree =
    walk-to-root-Directed-Tree directed-tree-Enriched-Directed-Tree

  unique-direct-successor-Enriched-Directed-Tree :
    unique-direct-successor-Directed-Graph
      graph-Enriched-Directed-Tree
      root-Enriched-Directed-Tree
  unique-direct-successor-Enriched-Directed-Tree =
    unique-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree

  unique-direct-successor-is-proper-node-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-proper-node-Enriched-Directed-Tree x →
    is-contr ( Σ node-Enriched-Directed-Tree (edge-Enriched-Directed-Tree x))
  unique-direct-successor-is-proper-node-Enriched-Directed-Tree =
    unique-direct-successor-is-proper-node-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  is-proof-irrelevant-direct-successor-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-proof-irrelevant
      ( Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x))
  is-proof-irrelevant-direct-successor-Enriched-Directed-Tree =
    is-proof-irrelevant-direct-successor-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  is-prop-direct-successor-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    is-prop
      ( Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x))
  is-prop-direct-successor-Enriched-Directed-Tree =
    is-prop-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree

  eq-direct-successor-Enriched-Directed-Tree :
    {x : node-Enriched-Directed-Tree}
    ( u v : Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x)) →
    u ＝ v
  eq-direct-successor-Enriched-Directed-Tree =
    eq-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree

  direct-successor-is-proper-node-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    ¬ (is-root-Enriched-Directed-Tree x) →
    Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x)
  direct-successor-is-proper-node-Enriched-Directed-Tree =
    direct-successor-is-proper-node-Directed-Tree
      directed-tree-Enriched-Directed-Tree

  shape-Enriched-Directed-Tree : node-Enriched-Directed-Tree → A
  shape-Enriched-Directed-Tree = pr1 (pr2 T)

  shape-root-Enriched-Directed-Tree : A
  shape-root-Enriched-Directed-Tree =
    shape-Enriched-Directed-Tree root-Enriched-Directed-Tree

  enrichment-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    B (shape-Enriched-Directed-Tree x) ≃
    Σ (node-Enriched-Directed-Tree) (λ y → edge-Enriched-Directed-Tree y x)
  enrichment-Enriched-Directed-Tree = pr2 (pr2 T)

  map-enrichment-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) →
    B (shape-Enriched-Directed-Tree x) →
    direct-predecessor-Enriched-Directed-Tree x
  map-enrichment-Enriched-Directed-Tree x =
    map-equiv (enrichment-Enriched-Directed-Tree x)

  node-enrichment-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) (b : B (shape-Enriched-Directed-Tree x)) →
    node-Enriched-Directed-Tree
  node-enrichment-Enriched-Directed-Tree x b =
    pr1 (map-enrichment-Enriched-Directed-Tree x b)

  edge-enrichment-Enriched-Directed-Tree :
    (x : node-Enriched-Directed-Tree) (b : B (shape-Enriched-Directed-Tree x)) →
    edge-Enriched-Directed-Tree (node-enrichment-Enriched-Directed-Tree x b) x
  edge-enrichment-Enriched-Directed-Tree x b =
    pr2 (map-enrichment-Enriched-Directed-Tree x b)

  coherence-square-map-enrichment-Enriched-Directed-Tree :
    {x y : node-Enriched-Directed-Tree} (p : x ＝ y) →
    coherence-square-maps
      ( tr B (ap shape-Enriched-Directed-Tree p))
      ( map-enrichment-Enriched-Directed-Tree x)
      ( map-enrichment-Enriched-Directed-Tree y)
      ( tot ( λ y → tr (edge-Enriched-Directed-Tree y) p))
  coherence-square-map-enrichment-Enriched-Directed-Tree refl = refl-htpy