The universal tree

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.
Last modified on 2025-10-31.

{-# OPTIONS --guardedness #-}

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

Idea

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

  X ↦ Σ (T : 𝒰), (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

Recent changes