## Stream: maths

### Topic: Cotactic

#### Brendan Seamas Murphy (Dec 15 2019 at 00:58):

Is there a tactic which can prove the dual of a categorical statement? If not, does anybody know prior work (e.g. did someone do this in Coq)?

#### Reid Barton (Dec 15 2019 at 01:01):

No, not yet. We discussed this a long time ago, but there were hardly any examples to apply it to then.

#### Brendan Seamas Murphy (Dec 15 2019 at 01:09):

I'm thinking of doing some abelian category stuff, and this feels like it would be important for quality of life there. I might look into implementing it but it seems tricky

#### Reid Barton (Dec 15 2019 at 01:23):

It probably is tricky. Are you familiar with to_additive? It may make sense to do something similar to that

#### Kevin Buzzard (Dec 15 2019 at 10:20):

One limit of to_additive is that, if I understand correctly, there's no capability for changing the order of inputs. In particular moving from x^n to n \bub x can't be done automatically. This will be much worse in the limit/colimits situation so a baby problem would be to make to_additive handle powers.

Last updated: May 12 2021 at 08:14 UTC