agda
Revisiting Dagger Categories
There's an interesting discussion about a "proper categorical" definition of dagger category by Peter LeFanu Lumsdaine (see the first answer). So I wonder if this should have any impact on the definition here? (@Taneb ?)
Somehow, the current definition doesn't seem to violate the principle of equivalence anywhere (there certainly are no object-level conditions present).
I've got a feeling that I'm cheating somehow with that definition. The type of _† : ∀ {A B} → A ⇒ B → B ⇒ A might be imposing equalities on the objects according to the relevant definitions, it's certainly equivalent to having some functor from C to op C and imposing the equalities after-the-fact, this way is just easier to write and implement.
I'm not sure if we need to use the "proper categorical" definition, but if there's interest I'm not going to get in the way. (If you can convince me - and I'm willing to be convinced here - that the current definition is definitely not what we want, then I'll implement this definition)
