Duality principle in category theory

Stream: Is there code for X?

[Coriver Chen]

Hi is there any lemma characterizing the dual principal in category theory?

[Coriver Chen]

for example, with which one can prove epi_of_epi from mono_of_mono or vice versa

[Scott Morrison]

Not really? I'm sure the lemma relating epis in C with monos in C dual is there somewhere.

But sadly there is no analogue of the @[to_additive] attribute for duality that "knows" about this.

[Yaël Dillies]

@Matthieu PIQUEREZ talked about something like that in his recent talk.

[Scott Morrison]

The "duality principle" is not really a theorem. There's a perfectly good "metatheorem" that could be (but hasn't been) reflected in helpful tactics.

[Yaël Dillies]

Same thing for order theory, really

[Scott Morrison]

And for both, the annoying thing about making a nice tactic is that it's in practice hard to specify which things to dualize and which things to leave alone in any given setting.

[Yaël Dillies]

I think "dualise everything on type α where α is a free variable" is a reasonable ask.

[Yaël Dillies]

That's a bit naive as an approach and might need to be run $2^n - 1$ times (where $n$ is the number of free variable types) but it's better than nothing.

[Coriver Chen]

Got it, thank you very much:D