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 universal tree

{-# OPTIONS --guardedness #-}

module trees.universal-tree where
Imports 
open import foundation.universe-levels

Idea

The universal tree is the coinductive type associated to the polynomial endofunctor

  X ↦ Σ 𝒰 (λ T → Xᵀ).

Note that this is the same polynomial endofunctor that we used to define the type of multisets, which is the universal well-founded tree.

Definitions

The universal tree of small trees

module _
  (l : Level)
  where

  record Universal-Tree : UU (lsuc l)
    where
    coinductive
    field
      type-Universal-Tree :
        UU l
      branch-Universal-Tree :
        (x : type-Universal-Tree) → Universal-Tree

  open Universal-Tree public