How would the implementation of a general equivalence relation work? Just defining the equivalence relation does not yield a method for chosing a representative. Would you check the equivalence at each operation?
-- ogf(c,x) = Σ n:ℕ, cₙ xⁿ
def ogf (c : ℕ → ℕ) (α : Type) :=
Σ n:ℕ, fin (c n) × (fin n → α)
For example list has coefficients Cn = {1,1,1,1...}
inductive list (α : Type)
| nil : list
| cons (hd : α) (tl : list) : list
inductive bin_tree (α : Type)
| leaf : bin_tree
| branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree
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.
Choosing a canonical representative is not feasible in the general case, so yes one would need to prove that every operation respects the equivalence relation.
Do you demand that f(x) ~ x implies that f(x) = x ? (~ being the equivalence and = being identity).