Function.Equiv

Stream: lean4

[François G. Dorais]

In Init/Core.lean, there is a declaration of Function.Equiv for the proof of funext. The definition is not protected, which is an annoying source of conflict since Equiv is a rather common name and the Function namespace has multiple other uses.

Would protecting Function.Equiv be a welcome PR? This is a very local change, just a few lines in Init/Core.lean, since the relation has almost no use case after the proof of funext.

[François G. Dorais]

Alternatively, it could be renamed EquivExt or something else which is not prone to name collision.

[Mario Carneiro]

+1 from me. That definition is entirely contained to the proof of funext, and AFAIK it is not referred to at all in mathlib, so it could even be private. Protected also works, since no one is going to use Function.Equiv by that name by accident.

[François G. Dorais]

I'm going ahead with a PR since it's only four lines of code in one file...

[François G. Dorais]

Leo merged the PR. Thanks!