search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Revisiting Dagger Categories #311

Open JacquesCarette opened 2 years ago

JacquesCarette commented 2 years ago

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

Taneb commented 2 years ago

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)

Taneb commented 1 year ago

nLab has some relevant discussion here: https://ncatlab.org/nlab/show/identity-on-objects+functor

JacquesCarette commented 1 year ago

Did you notice that I implemented IOO Functors? So maybe that could be used.

Taneb commented 1 year ago

I hadn't noticed that! Yes, that looks like it could be used.