search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

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

Open fredrik-bakke opened 7 months ago

fredrik-bakke commented 7 months ago

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.

EgbertRijke commented 7 months ago

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.

fredrik-bakke commented 7 months ago

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.