Big dagger-category to-do list

[Taneb]

Notwithstanding #311, this are things I want to see implemented regarding dagger categories, mostly taken from Karvonen's The Way of the Dagger

• Dagger functors
• Category of dagger categories, dagger functors, and natural transformations
• Dagger functor categories
• Dagger 2-categories
• DagCat is a dagger 2-category
• (braided, symmetric) monoidal dagger categories (Karvonnen doesn't mention braided monoidal categories at all)
• dagger Frobenius monoids
• Dagger equivalences in dagger 2-categories
• Dagger adjunctions
• Dagger limits
• Rig dagger categories
• Dagger Frobenius monads
• Dagger adjunctions produce dagger Frobenius monads
• Kleisli categories of dagger Frobenius monads are dagger categories
• More...?