agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Idea: refactor categories to build on the theory of wild categories

Open fredrik-bakke opened this issue 2 years ago • 2 comments

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.

fredrik-bakke avatar Nov 22 '23 19:11 fredrik-bakke

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.

EgbertRijke avatar Nov 25 '23 21:11 EgbertRijke

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.

fredrik-bakke avatar Nov 26 '23 14:11 fredrik-bakke