# Zulip Chat Archive

## Stream: new members

### Topic: Instances and coercion

#### Nicolò Cavalleri (Aug 23 2020 at 17:49):

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 (Aug 23 2020 at 22:10):

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

maybe

#### Scott Morrison (Aug 23 2020 at 23:22):

I'm not sure your question makes sense. There's content: you need to know that the product of two `bar`

s which came from `foo`

s can be given the additional structure of a `foo`

.

#### Nicolò Cavalleri (Aug 24 2020 at 12:47):

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 (Aug 24 2020 at 12:52):

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 (Aug 24 2020 at 15:16):

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 (Aug 24 2020 at 15:16):

(Are lifts through equivalences generally defined?)

Last updated: May 16 2021 at 05:21 UTC