Instances and coercion

Stream: new members

[Nicolò Cavalleri]

Suppose I have to structures, foo and bar, such that foo extends bar and there is a coercion from foo to bar. If there's an instance of e.g. comm_group bar, what is the easiest and quickest way to transfer it to foo?

[Kevin Buzzard]

instance : comm_group foo := { ..bar.comm_group} maybe

[Scott Morrison]

I'm not sure your question makes sense. There's content: you need to know that the product of two bars which came from foos can be given the additional structure of a foo.

[Nicolò Cavalleri]

Yes you are right but the whole proof of this is in the has_mul instance. Is there not a way to do the rest in like one line? In any case this was the wrong example, I wrote a random class but I was thinking more of classes like partial_order where you have an induced order and you do not need to prove anything for it.

[Reid Barton]

Nicolò Cavalleri said:

Yes you are right but the whole proof of this is in the has_mul instance.

Well, no--you have to prove the new function is associative, and that the identity is a foo, and so on. (From the rest of your message I'm guessing foo extends bar with extra properties only and not extra data, but you didn't mention this.)

Is there not a way to do the rest in like one line? In any case this was the wrong example, I wrote a random class but I was thinking more of classes like partial_order where you have an induced order and you do not need to prove anything for it.

For a partial order, you can use docs#partial_order.lift if you have an injection foo -> bar.
In general, this procedure depends on the nature of the class (partial_order here).

[Nicolò Cavalleri]

What about lifting instances through equivalences? Is there a general way to do it under possibly some additional hypotheses or should I manually define a lift for the structures I'm intrested in?

[Nicolò Cavalleri]

(Are lifts through equivalences generally defined?)