Equiv.refl without argument

Stream: mathlib4

[Martin Dvořák]

Should there be an alternative to Equiv.refl that doesn't require explicit argument?
The way I deal with it is

notation "=.≃" => Equiv.refl _

but maybe there should be something for all Mathlib users.

[Edward van de Meent]

i made a PR like that once (adding Equiv.rfl and the like for a bunch of such structures) (#29118). the main reaction was "we probably don't want that for defs"

[Aaron Liu]

It could be a notation

[Martin Dvořák]

Edward van de Meent said:

i made a PR like that once (adding Equiv.rfl and the like for a bunch of such structures) (#29118). the main reaction was "we probably don't want that for defs"

It it about Equiv or Equivalence or both?

[Edward van de Meent]

ah, it's about things in the CategoryTheory corner, meaning CategoryTheory.Iso, CategoryTheory.Equivalence and similar. not Equiv. Still, i suspect that the issues raised aren't specific to categories

[Martin Dvořák]

I guess so. I simply love chaining the dot notation.