agda-unimath
agda-unimath copied to clipboard
Idea: refactor categories to build on the theory of wild categories
This seems appropriate following the discussion with Anders after #910 that "properties", of categories should be separated from its "data", and allows us to repeat fewer arguments.
It is not yet clear to me that data should be separated from properties, as is implied, but we can definitely discuss this idea further.
Oh, yes, I am not yet convinced by this idea either; I should have phrased the issue text differently. I still think this refactoring makes a lot of sense, though.