This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The coalgebra of directed trees

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