Idea: refactor (nonunital) precategories to have both directions of the associativity witness
fredrik-bakke opened this issue · 1 comments
fredrik-bakke commented
This allows the opposite category construction to be a definitional involution as remarked by Egbert and Anders. This is very useful due to the central importance of this particular construction.
fredrik-bakke commented
on second thought, this actually shouldn't be very hard to implement.