cata for N mutually-recursive types

CataI.agda

open import Data.List using (List; _∷_; [])
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Show renaming (show to showℕ)
open import Data.String
open import Relation.Binary.PropositionalEquality

{-# NO_POSITIVITY_CHECK #-}
data FixI {Index : Set} (f : (Index → Set) → (Index → Set)) (i : Index) : Set where
  InI
    : f (FixI f) i
    → FixI f i

{-# TERMINATING #-}
cataI
  : {Index : Set}
  → (f : (Index → Set) → (Index → Set))
  → (map : {a b : Index → Set}
         → (∀ i → a i → b i)
         → (i : Index)
         → f a i → f b i)
  → (a : Index → Set) 
  → (∀ i → f a i → a i)
  → (i : Index)
  → FixI f i
  → a i
cataI f map a alg i (InI fFix)
  = alg i (map (cataI f map a alg) i fFix)


data Index : Set where
  TreeIndex
    : Index
  ForestIndex
    : Index

data TreeF (e : Set) (r : Index → Set) : Index → Set where
  Node
    : e
    → r ForestIndex
    → TreeF e r TreeIndex
  Nil
    : TreeF e r ForestIndex
  Cons
    : r TreeIndex
    → r ForestIndex
    → TreeF e r ForestIndex

mapTreeF
  : {e : Set}
  → {a b : Index → Set}
  → (∀ i → a i → b i)
  → (i : Index)
  → TreeF e a i
  → TreeF e b i
mapTreeF f TreeIndex (Node e forest)
  = Node e (f ForestIndex forest)
mapTreeF _ ForestIndex Nil
  = Nil
mapTreeF f ForestIndex (Cons tree forest)
  = Cons (f TreeIndex tree) (f ForestIndex forest)

Tree : Set → Set
Tree e = FixI (TreeF e) TreeIndex

Forest : Set → Set
Forest e = FixI (TreeF e) ForestIndex

showTree
  : ∀ {e}
  → (e → String)
  → Tree e → String
showTree {e} showE = cataI (TreeF e) mapTreeF (λ _ → String) go TreeIndex
  where
    go : (i : Index) → TreeF e (λ _ → String) i → String
    go TreeIndex (Node e ss)
      = "Node " ++ showE e ++ " [" ++ ss ++ "]"
    go ForestIndex Nil
      = ""
    go ForestIndex (Cons s "")
      = s
    go ForestIndex (Cons s ss)
      = s ++ ", " ++ ss

nil : ∀ {e} → Forest e
nil = InI Nil

cons : ∀ {e} → Tree e → Forest e → Forest e
cons tree forest = InI (Cons tree forest)

mkForest : ∀ {e} → List (Tree e) → Forest e
mkForest []
  = nil
mkForest (t ∷ ts)
  = cons t (mkForest ts)

node : ∀ {e} → e → List (Tree e) → Tree e
node e ts = InI (Node e (mkForest ts))

testShowTree : showTree showℕ (node 1 (node 2 [] ∷  node 3 [] ∷ []))
             ≡ "Node 1 [Node 2 [], Node 3 []]"
testShowTree = refl