Heterogenous trees

HetTrees.agda

data List {α} : Set α → Set α where
  [] : ∀ {X} → List X
  _::_ : ∀ {X} → X → List X → List X

map : ∀ {α β} → {A : Set α} → {B : Set β} →
      (f : A → B) → List A → List B
map f [] = []
map f (x :: xs) = f x :: map f xs

data hList {α} : List (Set α) → Set α where
  [] : hList []
  _::_ : {l : List (Set α)} → {A : Set α} →
         (x : A) → hList l →
         hList (A :: l)

data BinTree {α} (A : Set α) : Set α where
  [] : BinTree A
  bt : (x : A) → (l : BinTree A) → (r : BinTree A) → BinTree A

data hBinTree {α} : BinTree (Set α) → Set α where
  [] : hBinTree []
  bt : {l r : BinTree (Set α)} → {A : Set α} →
       (x : A) → hBinTree l → hBinTree r →
       hBinTree (bt A l r)

data RoseTree {α} (A : Set α) : Set α where
  rose : A → List (RoseTree A) → RoseTree A

{-# NO_POSITIVITY_CHECK #-}

data hRoseTree {α} : RoseTree (Set α) → Set α where
  hrose : {lt : List (RoseTree (Set α))} → {A : Set α} →
          (x : A) → hList (map hRoseTree lt) →
          hRoseTree (rose A lt)