Typeclasses and structures and untangling myself

Stream: lean4

[Wrenna Robson]

In something I am doing, I somewhat want to make the following definition.

abbrev ControlBitsLayer (m : ℕ) := Fin (2^m) → Bool

class CBType (α : ℕ → Type*) where
  zero : α 0 ≃ ControlBitsLayer 0
  weave m : α (m + 1) ≃ (ControlBitsLayer (m + 1) × ControlBitsLayer (m + 1)) × (Bool → α m)

def cbTypeEquiv [CBType α] [CBType β] : α m ≃ β m :=
m.recOn (CBType.zero.trans CBType.zero.symm)
  (fun n IE => (CBType.weave n).trans
    (((Equiv.refl _).prodCongr  ((Equiv.refl _).arrowCongr IE)).trans
      (CBType.weave n).symm))

Conceptually the idea is that I want to define something for types of a "class" CBType, or more properly I suppose I have types parameterised by a natural number, which obey some nice inductive property as illustrated here. I want to do something that only uses this property of them - if I can show such a type has a "zero" and a "weave", that's enough and I can work with that. And conceptually this means that the types are (parametrically?) equivalent.

The trouble is, as you can probably tell by this confused explanation, is that I am falling over myself with the meta level of all this. I'm not even certain defining this as a class is the right choice - perhaps defining it as a structure is? Has anyone got any thoughts on how I migh tuntangle my thinking?