Definition depth {s: sorts σ}: term σ s → nat := term_ind (λ _ _, nat) (λ (nm: names σ) (v: (term σ)⋆ (arity nm)) (depths: hvec (h1map_vec (λ _ _, nat) v)), 1 + h2foldr (λ _ _, max) 0 depths).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.