[hiker]

If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some coefficients C : N->N:

  -- ogf(c,x) = Σ n:ℕ, cₙ xⁿ
  def ogf (c : ℕ → ℕ) (α : Type) :=
  Σ n:ℕ, fin (c n) × (fin n → α)

(fin n is finite type with exactly n elements)

For example list has coefficients Cn = {1,1,1,1...}

  inductive list (α : Type)
  | nil : list
  | cons (hd : α) (tl : list) : list

and binary trees

  inductive bin_tree (α : Type)
  | leaf : bin_tree
  | branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree

have coefficients the Catalan numbers {1,1,2,5,14,42,132,429,...}.

Computing those coefficients from a type definition is not always trivial though (see the symbolic method http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf).

This can be extended to infinite data structures too by switching the natural numbers to ordinal numbers in the ogf definition.