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
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