Why don't use EquivFunctor?

Stream: lean4

[Vasilii Nesterov]

Hi there! I wonder why in Mathlib we so rarely use EquivFunctor. Most classes are in fact EquivFunctors, and this could allow us to tranfser results (in particular, instances) between equivalent types. For example instead

instance completeAtomicBooleanAlgebra (α : Type _)  : CompleteAtomicBooleanAlgebra (Set α) :=
  { instBooleanAlgebraSet with
    le_sSup := fun s t t_in a a_in => ⟨t, t_in, a_in⟩
    sSup_le := fun s t h a ⟨t', ⟨t'_in, a_in⟩⟩ => h t' t'_in a_in
    le_sInf := fun s t h a a_in t' t'_in => h t' t'_in a_in
    sInf_le := fun s t t_in a h => h _ t_in
    iInf_iSup_eq := by intros; ext; simp [Classical.skolem] }

we could have

instance : EquivFunctor CompleteAtomicBooleanAlgebra := by sorry

-- transfer instance from (β → Prop) to Set β
instance (β : Type _) : CompleteAtomicBooleanAlgebra (Set β) := by
  apply EquivFunctor.map (α := β → Prop)
  · exact?
  · infer_instance

Also, I think EquivFunctor can be derived automatically. Am I missing something?

[Kim Morrison]

No, you're not, and I worked on this for a while back in Lean 3 days.

The basic answer is that the payoff is actually quite limited, and so no one has invested the time to set up automation.

It's also somewhat delicate to make sure that instances constructed via transfer have the exact defeqs you're after.