opposite

Stream: lean4

[Reid Barton]

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]

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]

It sounds possible, but not that pleasant.