The coalgebra of directed trees

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-03.
Last modified on 2023-05-16.

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

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

Idea

Using the fibers of base elements, the type of directed trees, of which the type of nodes and the types of edges are of the same universe level, has the structure of a coalgebra for the polynomial endofunctor

  A ↦ Σ (X : UU), X → A

Definition

coalgebra-Directed-Tree :
  (l : Level) → coalgebra-polynomial-endofunctor (lsuc l) (UU l) (λ X → X)
pr1 (coalgebra-Directed-Tree l) = Directed-Tree l l
pr1 (pr2 (coalgebra-Directed-Tree l) T) = base-Directed-Tree T
pr2 (pr2 (coalgebra-Directed-Tree l) T) = fiber-base-Directed-Tree T

Recent changes