adjunctions in bicategories

Stream: Is there code for X?

[Mike Shulman]

Does mathlib contain definitions and properties of internal adjunctions in a bicategory?

[Scott Morrison]

Unfortunately no. We have some basic material on rigid categories.

[Mike Shulman]

Ok, thanks. Maybe I will have some students work on it.

[Scott Morrison]

Oh, @Mike Shulman, sorry I had forgotten about this: #13418.

[Mike Shulman]

Thanks! What's the status of it? It looks like it hasn't been updated for
a year?

[Adam Topaz]

Presumably at this point it could just be redone in mathlib4. I think all the requirements have been ported.

[Adam Topaz]

Oh, maybe the coherence tactic hasn’t been ported yet?

[Matthew Ballard]

No but it is only two files away