AG
рекурсивным деревом типов впрочем в приципе можно назвать inductive type family
rec : {a : Type} -> a -> ( Nat -> a -> a ) -> Nat -> a
а индуктор ind : {p : Nat -> Type} -> p Z -> ((k : Nat) -> p k -> p (S k)) -> (n : Nat) -> p n