SizedTrees.agda

module SizedTrees where

open import Agda.Builtin.Size

data list (A : Set₀) : Set₀ where
  nil : list A
  cons : A → list A → list A

map : ∀{A B} → (A → B) → list A → list B
map f nil = nil
map f (cons a l) = cons (f a) (map f l)

data tree (A : Set₀) : Size → Set₀ where
  fork : ∀ {i} → A → list (tree A i) → tree A (↑ i)

map-tree : ∀ {i} {A B} → (A → B) → tree A i → tree B i
map-tree f (fork a l) = fork (f a) (map (map-tree f) l)