consider adding a symmetric version of associativity in the defintion of Category about agda-categories HOT 14 CLOSED

Sorry to show up late to the party, but could we add some comments in Categories.Category.Core to explain why sym-assoc is included? Newcomers to the library might be confused by the presence of this field.

from agda-categories.

93f7450

from agda-categories.

Hello, I'm that confused newcomer! Why is it important foe the opposite category of the opposite category to be definitionally equal to the original category?

in short, definitional equality is a blessing.

technically, it's more intuitive. think about a category C and its opposite. we usually think there are only two "sides" of a category. however, if op of op is just equivalent to C, then it means one can generate infinite number of categories by stacking ops. nonetheless, half of them is really the same as one and the other half is the same as another. so why would we prefer moving between op of op and C via a functor, the existence of which is purely caused by technical reasons? making things definitional is just cleaner. after all, you will have to show all limits, for example, is preserved by op of op etc, and that's just unnecessary burden to deal with.

from agda-categories.

@HuStmpHrrr do you maybe have a concrete example from the library where it simplifies things?

I can come up with some example where it might, but I haven't actually encountered one in practice (in the library) yet.

from agda-categories.

You mean as an additional field? If we can edide it 99% of the time, then that's worth considering. Maybe make it implicit?

from agda-categories.

yeah an additional field. just flip the direction of assoc. this way, op would just need to swap assoc and assoc-sym, and that makes op of op definitionally equal to the original category. this helps the cases where opposite category is used.

from agda-categories.

It is definitely worth a try - if it works, that would be a nice thing to have. But I think I'll let you conduct that experiment...

from agda-categories.

OK so it looks good. for some reason Category needs to have eta-equality explicitly turned on. I thought this option is one by default.

from agda-categories.

Definitely something to document in the design decisions.
And yes, I thought eta-equality was on by default too - a bug?

from agda-categories.

not sure, I will figure out a minimal reproducible case and ask if that's expected.

from agda-categories.

c.f. agda/agda#4142

from agda-categories.

sure that's not a problem. in fact, many libraries in Coq have this setup too.

from agda-categories.

Hello, I'm that confused newcomer! Why is it important foe the opposite category of the opposite category to be definitionally equal to the original category?

from agda-categories.

here is one usage of that: b2cd7aa#diff-6218f7f546559e9086b91e1f79ed1fc5L63

from agda-categories.