The underlying trees of elements of coalgebras of polynomial endofunctors

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-03.
Last modified on 2024-02-06.

module trees.underlying-trees-elements-coalgebras-polynomial-endofunctors where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.binary-transport
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.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.isolated-elements
open import foundation.negated-equality
open import foundation.propositions
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-empty-type
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.coalgebras-polynomial-endofunctors
open import trees.combinator-directed-trees
open import trees.combinator-enriched-directed-trees
open import trees.directed-trees
open import trees.elementhood-relation-coalgebras-polynomial-endofunctors
open import trees.enriched-directed-trees
open import trees.equivalences-directed-trees
open import trees.equivalences-enriched-directed-trees

Idea

For every element x of a coalgebra of a polynomial endofunctor we can inductively define an enriched directed tree. This tree is called the underlying enriched directed tree of x.

Definition

The underlying graph of an element of a coalgebra of a polynomial endofunctor

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  data
    node-element-coalgebra :
      type-coalgebra-polynomial-endofunctor X → UU (l2 ⊔ l3)
    where
    root-coalgebra :
      (w : type-coalgebra-polynomial-endofunctor X) →
      node-element-coalgebra w
    node-inclusion-element-coalgebra :
      {u v : type-coalgebra-polynomial-endofunctor X} →
      (u ∈ v in-coalgebra X) →
      node-element-coalgebra u →
      node-element-coalgebra v

  data
    edge-element-coalgebra :
      (w : type-coalgebra-polynomial-endofunctor X)
      (x y : node-element-coalgebra w) → UU (l2 ⊔ l3)
    where
    edge-to-root-element-coalgebra :
      {u v : type-coalgebra-polynomial-endofunctor X}
      (H : u ∈ v in-coalgebra X) →
      edge-element-coalgebra v
        ( node-inclusion-element-coalgebra H
          ( root-coalgebra u))
        ( root-coalgebra v)
    edge-inclusion-element-coalgebra :
      {u v : type-coalgebra-polynomial-endofunctor X}
      (H : u ∈ v in-coalgebra X) →
      {x y : node-element-coalgebra u}
      (e : edge-element-coalgebra u x y) →
      edge-element-coalgebra v
        ( node-inclusion-element-coalgebra H x)
        ( node-inclusion-element-coalgebra H y)

  graph-element-coalgebra :
    type-coalgebra-polynomial-endofunctor X →
    Directed-Graph (l2 ⊔ l3) (l2 ⊔ l3)
  pr1 (graph-element-coalgebra w) =
    node-element-coalgebra w
  pr2 (graph-element-coalgebra w) =
    edge-element-coalgebra w

  walk-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x y : node-element-coalgebra w) → UU (l2 ⊔ l3)
  walk-element-coalgebra w =
    walk-Directed-Graph (graph-element-coalgebra w)

The external graph of an element of a W-type

  node-external-graph-element-coalgebra :
    type-coalgebra-polynomial-endofunctor X → UU (l2 ⊔ l3)
  node-external-graph-element-coalgebra w =
    Σ ( type-coalgebra-polynomial-endofunctor X)
      ( λ u → walk-coalgebra-polynomial-endofunctor X u w)

  edge-external-graph-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x y : node-external-graph-element-coalgebra w) →
    UU (l2 ⊔ l3)
  edge-external-graph-element-coalgebra
    w (x , H) (y , K) =
    Σ ( x ∈ y in-coalgebra X) (λ e → cons-walk-Directed-Graph e K ＝ H)

  external-graph-element-coalgebra :
    type-coalgebra-polynomial-endofunctor X → Directed-Graph (l2 ⊔ l3) (l2 ⊔ l3)
  pr1 (external-graph-element-coalgebra w) =
    node-external-graph-element-coalgebra w
  pr2 (external-graph-element-coalgebra w) =
    edge-external-graph-element-coalgebra w

Properties

To be a root is decidable

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  is-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    node-element-coalgebra X w → UU (l2 ⊔ l3)
  is-root-element-coalgebra w x =
    root-coalgebra w ＝ x

  is-isolated-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    is-isolated (root-coalgebra {X = X} w)
  is-isolated-root-element-coalgebra w
    ( root-coalgebra w) =
    inl refl
  is-isolated-root-element-coalgebra w
    ( node-inclusion-element-coalgebra H y) =
    inr (λ ())

  is-contr-loop-space-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    is-contr
      ( root-coalgebra w ＝
        root-coalgebra w)
  is-contr-loop-space-root-element-coalgebra w =
    is-contr-loop-space-isolated-element
      ( root-coalgebra w)
      ( is-isolated-root-element-coalgebra w)

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

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  data
    Eq-node-element-coalgebra
      ( w : type-coalgebra-polynomial-endofunctor X) :
      ( x y : node-element-coalgebra X w) → UU (l2 ⊔ l3)
    where
    root-refl-Eq-node-element-coalgebra :
      Eq-node-element-coalgebra w
        ( root-coalgebra w)
        ( root-coalgebra w)
    node-inclusion-Eq-node-element-coalgebra :
      {u : type-coalgebra-polynomial-endofunctor X}
      (H : u ∈ w in-coalgebra X)
      {x y : node-element-coalgebra X u} →
      Eq-node-element-coalgebra u x y →
      Eq-node-element-coalgebra w
        ( node-inclusion-element-coalgebra H x)
        ( node-inclusion-element-coalgebra H y)

  refl-Eq-node-element-coalgebra :
    {w : type-coalgebra-polynomial-endofunctor X}
    (x : node-element-coalgebra X w) →
    Eq-node-element-coalgebra w x x
  refl-Eq-node-element-coalgebra
    ( root-coalgebra w) =
    root-refl-Eq-node-element-coalgebra
  refl-Eq-node-element-coalgebra
    ( node-inclusion-element-coalgebra {u} H x) =
    node-inclusion-Eq-node-element-coalgebra H
      ( refl-Eq-node-element-coalgebra x)

  center-total-Eq-node-element-coalgebra :
    {w : type-coalgebra-polynomial-endofunctor X}
    (x : node-element-coalgebra X w) →
    Σ ( node-element-coalgebra X w)
      ( Eq-node-element-coalgebra w x)
  pr1 (center-total-Eq-node-element-coalgebra x) = x
  pr2 (center-total-Eq-node-element-coalgebra x) =
    refl-Eq-node-element-coalgebra x

  contraction-total-Eq-node-element-coalgebra :
    {w : type-coalgebra-polynomial-endofunctor X}
    (x : node-element-coalgebra X w) →
    (u :
      Σ ( node-element-coalgebra X w)
        ( Eq-node-element-coalgebra w x)) →
    center-total-Eq-node-element-coalgebra x ＝ u
  contraction-total-Eq-node-element-coalgebra ._
    (._ , root-refl-Eq-node-element-coalgebra) =
    refl
  contraction-total-Eq-node-element-coalgebra ._
    ( .(node-inclusion-element-coalgebra H _) ,
      node-inclusion-Eq-node-element-coalgebra H e) =
    ap
      ( map-Σ
        ( λ z → Eq-node-element-coalgebra _ _ z)
        ( node-inclusion-element-coalgebra H)
        ( λ y →
          node-inclusion-Eq-node-element-coalgebra H))
      ( contraction-total-Eq-node-element-coalgebra _
        ( _ , e))

  is-torsorial-Eq-node-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    is-torsorial (Eq-node-element-coalgebra w x)
  pr1 (is-torsorial-Eq-node-element-coalgebra w x) =
    center-total-Eq-node-element-coalgebra x
  pr2 (is-torsorial-Eq-node-element-coalgebra w x) =
    contraction-total-Eq-node-element-coalgebra x

  Eq-eq-node-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    {x y : node-element-coalgebra X w} →
    x ＝ y → Eq-node-element-coalgebra w x y
  Eq-eq-node-element-coalgebra w refl =
    refl-Eq-node-element-coalgebra _

  is-equiv-Eq-eq-node-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x y : node-element-coalgebra X w) →
    is-equiv (Eq-eq-node-element-coalgebra w {x} {y})
  is-equiv-Eq-eq-node-element-coalgebra w x =
    fundamental-theorem-id
      ( is-torsorial-Eq-node-element-coalgebra w x)
      ( λ y → Eq-eq-node-element-coalgebra w {x} {y})

  extensionality-node-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x y : node-element-coalgebra X w) →
    (x ＝ y) ≃ Eq-node-element-coalgebra w x y
  pr1 (extensionality-node-element-coalgebra w x y) =
    Eq-eq-node-element-coalgebra w {x} {y}
  pr2 (extensionality-node-element-coalgebra w x y) =
    is-equiv-Eq-eq-node-element-coalgebra w x y

  eq-Eq-node-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x y : node-element-coalgebra X w) →
    Eq-node-element-coalgebra w x y → x ＝ y
  eq-Eq-node-element-coalgebra w x y =
    map-inv-equiv
      ( extensionality-node-element-coalgebra w x y)

Note that we don't expect that node-inclusion-element-coalgebra' is an embedding. The total space Σ (y : B x), node-element-coalgebra' (α y) embeds into node-element-coalgebra' (tree-coalgebra x α), and this implies that the node inclusion has the same truncation level as the fiber inclusions

  node-element-coalgebra' (α b) → Σ (y : B x), node-element-coalgebra' (α y)

In other words, the fiber is Ω (B , b).

For any u ∈-coalgebra v in coalgebra A B we have a graph inclusion from the underlying graph of u to the underlying graph of v

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  inclusion-element-coalgebra :
    {u v : type-coalgebra-polynomial-endofunctor X} →
    u ∈ v in-coalgebra X →
    hom-Directed-Graph
      ( graph-element-coalgebra X u)
      ( graph-element-coalgebra X v)
  pr1 (inclusion-element-coalgebra {u} {v} H) =
    node-inclusion-element-coalgebra H
  pr2
    ( inclusion-element-coalgebra {u} {v} H)
    x y e =
    edge-inclusion-element-coalgebra H e

  walk-inclusion-element-coalgebra :
    {u v : type-coalgebra-polynomial-endofunctor X} →
    (H : u ∈ v in-coalgebra X) →
    {x y : node-element-coalgebra X u} →
    walk-element-coalgebra X u x y →
    walk-element-coalgebra X v
      ( node-inclusion-element-coalgebra H x)
      ( node-inclusion-element-coalgebra H y)
  walk-inclusion-element-coalgebra {u} {v} H =
    walk-hom-Directed-Graph
      ( graph-element-coalgebra X u)
      ( graph-element-coalgebra X v)
      ( inclusion-element-coalgebra H)

The type of edges from the root of u ∈-coalgebra v to the root of v is contractible

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  is-contr-edge-to-root-element-coalgebra :
    {u v : type-coalgebra-polynomial-endofunctor X}
    (H : u ∈ v in-coalgebra X) →
    is-contr
      ( edge-element-coalgebra X v
        ( node-inclusion-element-coalgebra H
          ( root-coalgebra u))
        ( root-coalgebra v))
  pr1 (is-contr-edge-to-root-element-coalgebra H) =
    edge-to-root-element-coalgebra H
  pr2
    ( is-contr-edge-to-root-element-coalgebra H)
    ( edge-to-root-element-coalgebra .H) =
    refl

The type of edges from any node to the root is a proposition

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  is-proof-irrelevant-edge-to-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    is-proof-irrelevant
      ( edge-element-coalgebra X w x
        ( root-coalgebra w))
  is-proof-irrelevant-edge-to-root-element-coalgebra w ._
    ( edge-to-root-element-coalgebra H) =
    is-contr-edge-to-root-element-coalgebra X H

  is-prop-edge-to-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    is-prop
      ( edge-element-coalgebra X w x
        ( root-coalgebra w))
  is-prop-edge-to-root-element-coalgebra w x =
    is-prop-is-proof-irrelevant
      ( is-proof-irrelevant-edge-to-root-element-coalgebra
        w x)

The underlying graph of any element of a W-type is a directed tree

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  no-edge-from-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    is-empty
      ( Σ ( node-element-coalgebra X w)
          ( edge-element-coalgebra X w
            ( root-coalgebra w)))
  no-edge-from-root-element-coalgebra w (x , ())

  is-empty-eq-root-node-inclusion-element-coalgebra :
    {v w : type-coalgebra-polynomial-endofunctor X}
    (H : v ∈ w in-coalgebra X)
    (x : node-element-coalgebra X v) →
    root-coalgebra w ≠ node-inclusion-element-coalgebra H x
  is-empty-eq-root-node-inclusion-element-coalgebra
    H x ()

  has-unique-predecessor-node-inclusion-element-coalgebra :
    {v w : type-coalgebra-polynomial-endofunctor X}
    (H : v ∈ w in-coalgebra X)
    (x : node-element-coalgebra X v) →
    is-contr
      ( Σ ( node-element-coalgebra X w)
          ( edge-element-coalgebra X w
            ( node-inclusion-element-coalgebra H x)))
  pr1
    ( pr1
      ( has-unique-predecessor-node-inclusion-element-coalgebra H
        ( root-coalgebra w))) =
    root-coalgebra _
  pr2
    ( pr1
      ( has-unique-predecessor-node-inclusion-element-coalgebra H
        ( root-coalgebra w))) =
    edge-to-root-element-coalgebra H
  pr2
    ( has-unique-predecessor-node-inclusion-element-coalgebra H
      ( root-coalgebra w))
    ( ._ , edge-to-root-element-coalgebra .H) =
    refl
  pr1
    ( has-unique-predecessor-node-inclusion-element-coalgebra H
      ( node-inclusion-element-coalgebra K x)) =
    map-Σ
      ( λ y →
        edge-element-coalgebra X _
          ( node-inclusion-element-coalgebra H
            ( node-inclusion-element-coalgebra K x))
          ( y))
      ( node-inclusion-element-coalgebra H)
      ( λ y → edge-inclusion-element-coalgebra H)
      ( center
        ( has-unique-predecessor-node-inclusion-element-coalgebra K x))
  pr2
    ( has-unique-predecessor-node-inclusion-element-coalgebra H
      ( node-inclusion-element-coalgebra K x))
    ( .(node-inclusion-element-coalgebra H _) ,
      edge-inclusion-element-coalgebra .H f) =
    ap
      ( map-Σ _
        ( node-inclusion-element-coalgebra H)
        ( λ y → edge-inclusion-element-coalgebra H))
      ( eq-is-contr
        ( has-unique-predecessor-node-inclusion-element-coalgebra K x))

  has-unique-predecessor-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    is-contr
      ( ( root-coalgebra w ＝ x) +
        ( Σ ( node-element-coalgebra X w)
            ( edge-element-coalgebra X w x)))
  has-unique-predecessor-element-coalgebra w
    ( root-coalgebra w) =
    is-contr-equiv
      ( root-coalgebra w ＝
        root-coalgebra w)
      ( right-unit-law-coproduct-is-empty
        ( root-coalgebra w ＝
          root-coalgebra w)
        ( Σ ( node-element-coalgebra X w)
            ( edge-element-coalgebra X w
              ( root-coalgebra w)))
        ( no-edge-from-root-element-coalgebra w))
      ( is-contr-loop-space-root-element-coalgebra
        ( X)
        ( w))
  has-unique-predecessor-element-coalgebra w
    ( node-inclusion-element-coalgebra H x) =
    is-contr-equiv
      ( Σ ( node-element-coalgebra X w)
          ( edge-element-coalgebra X w
            ( node-inclusion-element-coalgebra H x)))
      ( left-unit-law-coproduct-is-empty
        ( root-coalgebra w ＝
          node-inclusion-element-coalgebra H x)
        ( Σ ( node-element-coalgebra X w)
            ( edge-element-coalgebra X w
              ( node-inclusion-element-coalgebra H x)))
        ( is-empty-eq-root-node-inclusion-element-coalgebra H x))
      ( has-unique-predecessor-node-inclusion-element-coalgebra H x)

  walk-to-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    walk-element-coalgebra X w x (root-coalgebra w)
  walk-to-root-element-coalgebra w
    ( root-coalgebra w) =
    refl-walk-Directed-Graph
  walk-to-root-element-coalgebra w
    ( node-inclusion-element-coalgebra {v} H x) =
    snoc-walk-Directed-Graph
      ( graph-element-coalgebra X w)
      ( walk-hom-Directed-Graph
        ( graph-element-coalgebra X v)
        ( graph-element-coalgebra X w)
        ( inclusion-element-coalgebra X H)
        ( walk-to-root-element-coalgebra v x))
      ( edge-to-root-element-coalgebra H)

  unique-walk-to-root-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    is-tree-Directed-Graph'
      ( graph-element-coalgebra X w)
      ( root-coalgebra w)
  unique-walk-to-root-element-coalgebra w =
    is-tree-unique-direct-successor-Directed-Graph'
      ( graph-element-coalgebra X w)
      ( root-coalgebra w)
      ( has-unique-predecessor-element-coalgebra w)
      ( walk-to-root-element-coalgebra w)

  directed-tree-element-coalgebra :
    type-coalgebra-polynomial-endofunctor X → Directed-Tree (l2 ⊔ l3) (l2 ⊔ l3)
  pr1 (directed-tree-element-coalgebra w) =
    graph-element-coalgebra X w
  pr1 (pr2 (directed-tree-element-coalgebra w)) =
    root-coalgebra w
  pr2 (pr2 (directed-tree-element-coalgebra w)) =
    unique-walk-to-root-element-coalgebra w

The underlying graph of an element of a W-type can be given the structure of an enriched directed tree

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  shape-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X) →
    node-element-coalgebra X w → A
  shape-element-coalgebra w
    ( root-coalgebra w) =
    shape-coalgebra-polynomial-endofunctor X w
  shape-element-coalgebra w
    ( node-inclusion-element-coalgebra {u} H y) =
    shape-element-coalgebra u y

  map-enrichment-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    B (shape-element-coalgebra w x) →
    Σ ( node-element-coalgebra X w)
      ( λ y → edge-element-coalgebra X w y x)
  pr1
    ( map-enrichment-element-coalgebra w
      ( root-coalgebra w) b) =
    node-inclusion-element-coalgebra
      ( b , refl)
      ( root-coalgebra (pr2 (pr2 X w) b))
  pr2
    ( map-enrichment-element-coalgebra w
      ( root-coalgebra w)
      ( b)) =
    edge-to-root-element-coalgebra (b , refl)
  map-enrichment-element-coalgebra w
    ( node-inclusion-element-coalgebra {u} H y) b =
    map-Σ
      ( λ z →
        edge-element-coalgebra X w z
          ( node-inclusion-element-coalgebra H y))
      ( node-inclusion-element-coalgebra H)
      ( λ z → edge-inclusion-element-coalgebra H)
      ( map-enrichment-element-coalgebra
        ( u)
        ( y)
        ( b))

  map-inv-enrichment-directed-tree-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    Σ ( node-element-coalgebra X w)
      ( λ y → edge-element-coalgebra X w y x) →
    B (shape-element-coalgebra w x)
  map-inv-enrichment-directed-tree-element-coalgebra w ._
    ( ._ , edge-to-root-element-coalgebra H) =
    pr1 H
  map-inv-enrichment-directed-tree-element-coalgebra w ._
    ( ._ ,
      edge-inclusion-element-coalgebra {u} H {x} {y} e) =
    map-inv-enrichment-directed-tree-element-coalgebra
      ( u)
      ( y)
      ( x , e)

  is-section-map-inv-enrichment-directed-tree-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    ( ( map-enrichment-element-coalgebra
        w x) ∘
      ( map-inv-enrichment-directed-tree-element-coalgebra
      w x)) ~ id
  is-section-map-inv-enrichment-directed-tree-element-coalgebra w ._
    ( ._ , edge-to-root-element-coalgebra (b , refl)) =
    refl
  is-section-map-inv-enrichment-directed-tree-element-coalgebra w ._
    ( ._ ,
      edge-inclusion-element-coalgebra {u} H {x} {y} e) =
    ap
      ( map-Σ
        ( λ z →
          edge-element-coalgebra X w z
            ( node-inclusion-element-coalgebra H y))
        ( node-inclusion-element-coalgebra H)
        ( λ z → edge-inclusion-element-coalgebra H))
      ( is-section-map-inv-enrichment-directed-tree-element-coalgebra u y
        ( x , e))

  is-retraction-map-inv-enrichment-directed-tree-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    ( map-inv-enrichment-directed-tree-element-coalgebra w x ∘
      map-enrichment-element-coalgebra w x) ~ id
  is-retraction-map-inv-enrichment-directed-tree-element-coalgebra w
    ( root-coalgebra w) b =
    refl
  is-retraction-map-inv-enrichment-directed-tree-element-coalgebra w
    ( node-inclusion-element-coalgebra {u} H y) b =
    is-retraction-map-inv-enrichment-directed-tree-element-coalgebra u y b

  is-equiv-map-enrichment-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    is-equiv (map-enrichment-element-coalgebra w x)
  is-equiv-map-enrichment-element-coalgebra w x =
    is-equiv-is-invertible
      ( map-inv-enrichment-directed-tree-element-coalgebra w x)
      ( is-section-map-inv-enrichment-directed-tree-element-coalgebra w x)
      ( is-retraction-map-inv-enrichment-directed-tree-element-coalgebra w x)

  enrichment-directed-tree-element-coalgebra :
    (w : type-coalgebra-polynomial-endofunctor X)
    (x : node-element-coalgebra X w) →
    B (shape-element-coalgebra w x) ≃
    Σ ( node-element-coalgebra X w)
      ( λ y → edge-element-coalgebra X w y x)
  pr1 (enrichment-directed-tree-element-coalgebra w x) =
    map-enrichment-element-coalgebra w x
  pr2 (enrichment-directed-tree-element-coalgebra w x) =
    is-equiv-map-enrichment-element-coalgebra w x

  enriched-directed-tree-element-coalgebra :
    type-coalgebra-polynomial-endofunctor X →
    Enriched-Directed-Tree (l2 ⊔ l3) (l2 ⊔ l3) A B
  pr1 (enriched-directed-tree-element-coalgebra w) =
    directed-tree-element-coalgebra X w
  pr1
    ( pr2 (enriched-directed-tree-element-coalgebra w)) =
    shape-element-coalgebra w
  pr2
    ( pr2 (enriched-directed-tree-element-coalgebra w)) =
    enrichment-directed-tree-element-coalgebra w

The underlying tree of w is the combinator tree of the underlying trees of component X w b indexed by b : B (shape w)

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  (w : type-coalgebra-polynomial-endofunctor X)
  where

  node-compute-directed-tree-element-coalgebra :
    node-element-coalgebra X w →
    node-combinator-Directed-Tree
      ( λ b → directed-tree-element-coalgebra X
        ( component-coalgebra-polynomial-endofunctor X w b))
  node-compute-directed-tree-element-coalgebra
    ( root-coalgebra w) =
    root-combinator-Directed-Tree
  node-compute-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (b , refl) x) =
    node-inclusion-combinator-Directed-Tree b x

  map-inv-node-compute-directed-tree-element-coalgebra :
    node-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b)) →
    node-element-coalgebra X w
  map-inv-node-compute-directed-tree-element-coalgebra
    root-combinator-Directed-Tree =
    root-coalgebra _
  map-inv-node-compute-directed-tree-element-coalgebra
    ( node-inclusion-combinator-Directed-Tree b x) =
    node-inclusion-element-coalgebra (b , refl) x

  is-section-map-inv-node-compute-directed-tree-element-coalgebra :
    ( node-compute-directed-tree-element-coalgebra ∘
      map-inv-node-compute-directed-tree-element-coalgebra) ~ id
  is-section-map-inv-node-compute-directed-tree-element-coalgebra
    root-combinator-Directed-Tree =
    refl
  is-section-map-inv-node-compute-directed-tree-element-coalgebra
    ( node-inclusion-combinator-Directed-Tree i x) =
    refl

  is-retraction-map-inv-node-compute-directed-tree-element-coalgebra :
    ( map-inv-node-compute-directed-tree-element-coalgebra ∘
      node-compute-directed-tree-element-coalgebra) ~ id
  is-retraction-map-inv-node-compute-directed-tree-element-coalgebra
    ( root-coalgebra w) =
    refl
  is-retraction-map-inv-node-compute-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (b , refl) x) =
    refl

  is-equiv-node-compute-directed-tree-element-coalgebra :
    is-equiv node-compute-directed-tree-element-coalgebra
  is-equiv-node-compute-directed-tree-element-coalgebra =
    is-equiv-is-invertible
      map-inv-node-compute-directed-tree-element-coalgebra
      is-section-map-inv-node-compute-directed-tree-element-coalgebra
      is-retraction-map-inv-node-compute-directed-tree-element-coalgebra

  equiv-node-compute-directed-tree-element-coalgebra :
    node-element-coalgebra X w ≃
    node-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b))
  pr1 equiv-node-compute-directed-tree-element-coalgebra =
    node-compute-directed-tree-element-coalgebra
  pr2 equiv-node-compute-directed-tree-element-coalgebra =
    is-equiv-node-compute-directed-tree-element-coalgebra

  edge-compute-directed-tree-element-coalgebra :
    (x y : node-element-coalgebra X w) →
    edge-element-coalgebra X w x y →
    edge-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b))
      ( node-compute-directed-tree-element-coalgebra x)
      ( node-compute-directed-tree-element-coalgebra y)
  edge-compute-directed-tree-element-coalgebra ._ ._
    ( edge-to-root-element-coalgebra (b , refl)) =
    edge-to-root-combinator-Directed-Tree b
  edge-compute-directed-tree-element-coalgebra ._ ._
    ( edge-inclusion-element-coalgebra (b , refl) e) =
    edge-inclusion-combinator-Directed-Tree b _ _ e

  map-inv-edge-compute-directed-tree-element-coalgebra' :
    ( x y :
      node-combinator-Directed-Tree
        ( directed-tree-element-coalgebra X ∘
          component-coalgebra-polynomial-endofunctor X w)) →
    edge-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b))
      ( x)
      ( y) →
    edge-element-coalgebra X w
      ( map-inv-node-compute-directed-tree-element-coalgebra x)
      ( map-inv-node-compute-directed-tree-element-coalgebra y)
  map-inv-edge-compute-directed-tree-element-coalgebra' ._ ._
    ( edge-to-root-combinator-Directed-Tree b) =
    edge-to-root-element-coalgebra (b , refl)
  map-inv-edge-compute-directed-tree-element-coalgebra' ._ ._
    ( edge-inclusion-combinator-Directed-Tree b x y e) =
    edge-inclusion-element-coalgebra (b , refl) e

  map-inv-edge-compute-directed-tree-element-coalgebra :
    ( x y : node-element-coalgebra X w) →
    edge-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b))
      ( node-compute-directed-tree-element-coalgebra x)
      ( node-compute-directed-tree-element-coalgebra y) →
    edge-element-coalgebra X w x y
  map-inv-edge-compute-directed-tree-element-coalgebra x y =
    ( binary-tr
      ( edge-element-coalgebra X w)
      ( is-retraction-map-inv-node-compute-directed-tree-element-coalgebra x)
      ( is-retraction-map-inv-node-compute-directed-tree-element-coalgebra y)) ∘
    ( map-inv-edge-compute-directed-tree-element-coalgebra'
      ( node-compute-directed-tree-element-coalgebra x)
      ( node-compute-directed-tree-element-coalgebra y))

  is-section-map-inv-edge-compute-directed-tree-element-coalgebra' :
    ( x y :
      node-combinator-Directed-Tree
        ( directed-tree-element-coalgebra X ∘
          component-coalgebra-polynomial-endofunctor X w)) →
    ( e :
      edge-combinator-Directed-Tree
        ( λ b →
          directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b))
        ( x)
        ( y)) →
    binary-tr
      ( edge-combinator-Directed-Tree
        ( λ b →
          directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b)))
      ( is-section-map-inv-node-compute-directed-tree-element-coalgebra x)
      ( is-section-map-inv-node-compute-directed-tree-element-coalgebra y)
      ( edge-compute-directed-tree-element-coalgebra
        ( map-inv-node-compute-directed-tree-element-coalgebra x)
        ( map-inv-node-compute-directed-tree-element-coalgebra y)
        ( map-inv-edge-compute-directed-tree-element-coalgebra' x y e)) ＝ e
  is-section-map-inv-edge-compute-directed-tree-element-coalgebra' ._ ._
    ( edge-to-root-combinator-Directed-Tree i) =
    refl
  is-section-map-inv-edge-compute-directed-tree-element-coalgebra' ._ ._
    ( edge-inclusion-combinator-Directed-Tree i x y e) =
    refl

  is-section-map-inv-edge-compute-directed-tree-element-coalgebra :
    (x y : node-element-coalgebra X w) →
    ( e :
      edge-combinator-Directed-Tree
        ( λ b →
          directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b))
        ( node-compute-directed-tree-element-coalgebra x)
        ( node-compute-directed-tree-element-coalgebra y)) →
    edge-compute-directed-tree-element-coalgebra x y
      ( map-inv-edge-compute-directed-tree-element-coalgebra x y e) ＝ e
  is-section-map-inv-edge-compute-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (b , refl) x)
    ( root-coalgebra _)
    ( e) =
    is-section-map-inv-edge-compute-directed-tree-element-coalgebra'
      ( node-compute-directed-tree-element-coalgebra _)
      ( node-compute-directed-tree-element-coalgebra _)
      ( e)
  is-section-map-inv-edge-compute-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (b , refl) x)
    ( node-inclusion-element-coalgebra (c , refl) y)
    ( e) =
    is-section-map-inv-edge-compute-directed-tree-element-coalgebra'
      ( node-compute-directed-tree-element-coalgebra _)
      ( node-compute-directed-tree-element-coalgebra _)
      ( e)

  is-retraction-map-inv-edge-compute-directed-tree-element-coalgebra :
    (x y : node-element-coalgebra X w) (e : edge-element-coalgebra X w x y) →
    map-inv-edge-compute-directed-tree-element-coalgebra x y
      ( edge-compute-directed-tree-element-coalgebra x y e) ＝ e
  is-retraction-map-inv-edge-compute-directed-tree-element-coalgebra ._ ._
    ( edge-to-root-element-coalgebra (b , refl)) = refl
  is-retraction-map-inv-edge-compute-directed-tree-element-coalgebra ._ ._
    ( edge-inclusion-element-coalgebra (b , refl) e) = refl

  is-equiv-edge-compute-directed-tree-element-coalgebra :
    (x y : node-element-coalgebra X w) →
    is-equiv (edge-compute-directed-tree-element-coalgebra x y)
  is-equiv-edge-compute-directed-tree-element-coalgebra x y =
    is-equiv-is-invertible
      ( map-inv-edge-compute-directed-tree-element-coalgebra x y)
      ( is-section-map-inv-edge-compute-directed-tree-element-coalgebra x y)
      ( is-retraction-map-inv-edge-compute-directed-tree-element-coalgebra x y)

  equiv-edge-compute-directed-tree-element-coalgebra :
    (x y : node-element-coalgebra X w) →
    edge-element-coalgebra X w x y ≃
    edge-combinator-Directed-Tree
      ( λ b →
        directed-tree-element-coalgebra X
          ( component-coalgebra-polynomial-endofunctor X w b))
      ( node-compute-directed-tree-element-coalgebra x)
      ( node-compute-directed-tree-element-coalgebra y)
  pr1 (equiv-edge-compute-directed-tree-element-coalgebra x y) =
    edge-compute-directed-tree-element-coalgebra x y
  pr2 (equiv-edge-compute-directed-tree-element-coalgebra x y) =
    is-equiv-edge-compute-directed-tree-element-coalgebra x y

  compute-directed-tree-element-coalgebra :
    equiv-Directed-Tree
      ( directed-tree-element-coalgebra X w)
      ( combinator-Directed-Tree
        ( λ b →
          directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b)))
  pr1 compute-directed-tree-element-coalgebra =
    equiv-node-compute-directed-tree-element-coalgebra
  pr2 compute-directed-tree-element-coalgebra =
    equiv-edge-compute-directed-tree-element-coalgebra

  shape-compute-enriched-directed-tree-element-coalgebra :
    shape-element-coalgebra X w ~
    ( ( shape-combinator-Enriched-Directed-Tree A B
        ( λ b →
          enriched-directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b))) ∘
      ( node-compute-directed-tree-element-coalgebra))
  shape-compute-enriched-directed-tree-element-coalgebra (root-coalgebra _) =
    refl
  shape-compute-enriched-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (b , refl) x) =
    refl

  enrichment-compute-enriched-directed-tree-element-coalgebra :
    (x : node-element-coalgebra X w) →
    htpy-equiv
      ( ( equiv-direct-predecessor-equiv-Directed-Tree
          ( directed-tree-element-coalgebra X w)
          ( combinator-Directed-Tree
            ( λ b →
              directed-tree-element-coalgebra X
                ( component-coalgebra-polynomial-endofunctor X w b)))
          ( compute-directed-tree-element-coalgebra)
          ( x)) ∘e
        ( enrichment-directed-tree-element-coalgebra X w x))
      ( ( enrichment-combinator-Enriched-Directed-Tree A B
          ( λ b →
            enriched-directed-tree-element-coalgebra X
              ( component-coalgebra-polynomial-endofunctor X w b))
          ( node-compute-directed-tree-element-coalgebra x)) ∘e
        ( equiv-tr B
          ( shape-compute-enriched-directed-tree-element-coalgebra x)))
  enrichment-compute-enriched-directed-tree-element-coalgebra
    ( root-coalgebra _)
    ( b) = refl
  enrichment-compute-enriched-directed-tree-element-coalgebra
    ( node-inclusion-element-coalgebra (c , refl) x) b =
    refl

  compute-enriched-directed-tree-element-coalgebra :
    equiv-Enriched-Directed-Tree A B
      ( enriched-directed-tree-element-coalgebra X w)
      ( combinator-Enriched-Directed-Tree A B
        ( λ b →
          enriched-directed-tree-element-coalgebra X
            ( component-coalgebra-polynomial-endofunctor X w b)))
  pr1 compute-enriched-directed-tree-element-coalgebra =
    compute-directed-tree-element-coalgebra
  pr1 (pr2 compute-enriched-directed-tree-element-coalgebra) =
    shape-compute-enriched-directed-tree-element-coalgebra
  pr2 (pr2 compute-enriched-directed-tree-element-coalgebra) =
    enrichment-compute-enriched-directed-tree-element-coalgebra

Recent changes