Cotactic

Stream: maths

[Brendan Seamas Murphy]

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]

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

[Brendan Seamas Murphy]

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]

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

[Kevin Buzzard]

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.