Can I Use `toFun` in the definition of `RelIso`?

Stream: mathlib4

[Lingwei Peng (彭灵伟)]

The definition of RelIso is:

structure RelIso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β where
  map_rel_iff' : ∀ {a b}, s (toEquiv a) (toEquiv b) ↔ r a b

There is a nested abstraction chain: FunLike → DFunLike → Function.Injective.
It’s like needing to learn real numbers before learning natural numbers.
Can I simplify this by directly using toFun instead, like so? Can I just use toFun instead

structure RelIso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β where
  map_rel_iff' : ∀ {a b}, s (toFun a) (toFun b) ↔ r a b

[Aaron Liu]

why would you want to do this

[Lingwei Peng (彭灵伟)]

I am building a small package called MySet for study purposes.

[Yury G. Kudryashov]

You can do that.

[Yury G. Kudryashov]

The definition in Mathlib doesn't do that because if you reuse an existing Equiv for the toEquiv projection, then the simp-normal form is e a, not e.toFun a.

[Lingwei Peng (彭灵伟)]

Thanks, I just realized that e.toFun a is only suitable for the initial stage, where the theorems are simple.