The coalgebra of enriched directed trees

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-03.
Last modified on 2025-10-31.

{-# OPTIONS --lossy-unification #-}

module trees.coalgebra-of-enriched-directed-trees where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import trees.coalgebras-polynomial-endofunctors
open import trees.enriched-directed-trees
open import trees.fibers-enriched-directed-trees
open import trees.polynomial-endofunctors

Idea

Using the fibers of base elements, the type of enriched directed trees has the structure of a coalgebra for the polynomial endofunctor

  X ↦ Σ (a : A), (B a → X).

Definition

module _
  {l1 l2 : Level} (l3 : Level) (P@(A , B) : polynomial-endofunctor l1 l2)
  where

  structure-coalgebra-Enriched-Directed-Tree :
    Enriched-Directed-Tree l3 l3 A B →
    type-polynomial-endofunctor P (Enriched-Directed-Tree l3 l3 A B)
  structure-coalgebra-Enriched-Directed-Tree T =
    ( shape-root-Enriched-Directed-Tree A B T ,
      fiber-base-Enriched-Directed-Tree A B T)

  coalgebra-Enriched-Directed-Tree :
    coalgebra-polynomial-endofunctor (l1 ⊔ l2 ⊔ lsuc l3) P
  coalgebra-Enriched-Directed-Tree =
    ( Enriched-Directed-Tree l3 l3 A B ,
      structure-coalgebra-Enriched-Directed-Tree)

Recent changes