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