type tag for "transfer instances along an equiv"?

Stream: general

[Yury G. Kudryashov]

We have various theorems of the form "if e : α ≃ β and β has some structure, then α has the same structure". What do you think about introducing a type tag get_instances_from e (of course, we need a better name), and turn these theorems into instances on the new type?

[Yury G. Kudryashov]

This way things in data.equiv.transfer_instance will be much less ugly than they are now.

[Johan Commelin]

cc @Scott Morrison

[Scott Morrison]

Sounds good.

[Yaël Dillies]

Also, could we maybe define the type tag in one file and then tag in their respective files?

[Yaël Dillies]

data.equiv.transfer_instances is quite an import dump right now.

[Yury G. Kudryashov]

The tag should be defined in data.equiv.basic and instances like docs#equiv.nonempty should be registered in this file.

[Yury G. Kudryashov]

Any suggestions about the name?

[Eric Wieser]

Can you give an example of what you want using this feature to look like? I don't understand the description

[Eric Wieser]

I also get the feeling that data.equiv.transfer_instance is used very rarely outside category theory anyway

[Yaël Dillies]

What about putting the instances in a locale as pointwise?

[Yury G. Kudryashov]

I want to have the following:

@[nolint unused_arguments]
def my_tag {α β : Type*} (e : α ≃ β) := α

variables {α β : Type*} (e : α ≃ β)
instance [inhabited β] : inhabited (my_tag e) := ⟨e.symm (default β)⟩
instance [has_one β] : has_one (my_tag e) := ⟨e.symm 0⟩
instance [has_mul β] : has_mul (my_tag e) := ⟨λ x y, e.symm (e x * e y)⟩
instance [semigroup β] : semigroup (my_tag e) :=
e.injective.semigroup _ (λ x y, e.apply_symm_apply _)

Here the last instance automatically finds has_mul (my_tag e).

[Yury G. Kudryashov]

@Yaël Dillies Why do you want to put them in a locale?

[Yaël Dillies]

I don't. Was mentioning it was an instance if ever we don't want them to pollute general typeclass inference.

[Yury G. Kudryashov]

They apply only to my_tag e, so this shouldn't be a problem.

[Yury G. Kudryashov]

With definitions above we can later write

instance [semigroup G] : semigroup (ulift G) := my_tag.semigroup equiv.ulift

[Eric Wieser]

Are there any situations where you wouldn't unfold my_tag like that?

[Eric Wieser]

Or is my_tag just an implementation detail that is always supposed to be unfolded by the user?

[Floris van Doorn]

Yury G. Kudryashov said:

With definitions above we can later write

instance [semigroup G] : semigroup (ulift G) := my_tag.semigroup equiv.ulift

How is this an improvement over the current equiv.ulift.semigroup?

[Eric Wieser]

I think the point is to eliminate the mess that is the implementation of src#equiv.semigroup:

let mul := e.has_mul in
by resetI; apply e.injective.semigroup _; intros; exact e.apply_symm_apply _

The lets wouldn't be necessary there if we were working with my_tag.

[Floris van Doorn]

Ah, that's fair.
@Yury G. Kudryashov's suggestion seems good to me.

[Yury G. Kudryashov]

What name should I use? Should instances be called my_tag.semigroup or just equiv.semigroup : semigroup (my_tag e)?

[Yury G. Kudryashov]

With the latter syntax, one can use letI : semigroup G := (e : G ≃ H).semigroup.

[Eric Wieser]

Maybe the type my_tag could be equiv.transfered_type?

[Floris van Doorn]

Or just equiv.domain?

[Eric Wieser]

I thought the direction we cared about wasdef codomain (e : α ≃ β) := β, for transferring instances "forward" along e from α to β?

[Yury G. Kudryashov]

Currently instances and lemmas transfer from β to α. I don't know why but I don't want to change it without a good reason.

[Eric Wieser]

In that case domain seems like a good suggestion to me