Naming of equivs

Stream: general

[Bryan Gin-ge Chen]

In #5263, @Eric Wieser suggests the following rename:

-def dart_equiv_sigma : G.dart ≃ Σ v, G.neighbor_set v :=
+def dart.to_sigma : G.dart ≃ Σ v, G.neighbor_set v :=

I think this is in keeping with some recent changes where we've been "upgrading" various functions to *_equivs while naming them after the function rather than including equiv. However, I think it'd be good to get some more opinions here (and maybe we could draft something about this for our naming conventions doc?).

[Bryan Gin-ge Chen]

The main point against this I suppose is that it might not then be immediately clear from the name that the declaration actually has extra structure and that we're using a coercion.

[Bhavik Mehta]

I think it could also be confusing to have two possible names for one thing: in some cases the equiv is called an equiv and other times it's named to_ as in the function, so whichever is decided on should be made consistent through mathlib if possible

[Eric Wieser]

In the context of a tactic state, the coercion is usually obvious thanks to \u= arrows everywhere

[Yury G. Kudryashov]

Naming it dart.to_sigma allows us to write x.to_sigma.

[Kyle Miller]

This particular equivalence only exists to establish a fintype that @[derive fintype] wasn't able to automatically handle. I don't think it's very useful outside of that, since (bending the API a little...) d.is_adj is definitionally a proof that d.snd is an element of G.neighbor_set d.fst.

I was thinking that this should have equiv in the name because the existence of the equivalence itself is what's important, where the examples in mathlib that use to_ seem to be functions with a built-in inverse. (Or I could inline it into the fintype instance to simplify the naming problem :smile:)