# Zulip Chat Archive

## Stream: lean4

### Topic: opposite

#### Reid Barton (Feb 03 2021 at 19:40):

So I tried making `opposite`

a structure. It's pretty rough, and a somewhat atypical situation, because we apply it to the objects of a category to form the opposite category, and those appear as parameters of the `hom`

types. So there are many cases where even the statements of existing lemmas no longer type check. Furthermore, the lost definitional equality `x.unop.op = x`

sometimes occurs when `x`

is not a variable but a more complicated expression, such as the application of a functor to an object.

#### Reid Barton (Feb 03 2021 at 19:42):

I guess the way we have dealt with such things elsewhere in the category theory library is to add "coherence isomorphisms", in this case between `x.unop.op`

and `x`

, and then provide `simp`

lemmas that say they are the identity if `x`

is of the form `y.op`

, and describing the behavior with respect to functors and inverses and so on.

#### Reid Barton (Feb 03 2021 at 19:42):

It sounds possible, but not that pleasant.

Last updated: May 18 2021 at 23:14 UTC