Well, if we follow the rabbit hole far enough, we end up with a requirement that may not hold in arbitrary categories?
Eg what is "-x"? If we were to apply algebra directly, it is such a type y such that x+y=0. I think non-trivial types never add up to 0, so "-x" cannot be defined for arbitrary categories.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2021-05-09 03:52 pm (UTC)Eg what is "-x"? If we were to apply algebra directly, it is such a type y such that x+y=0. I think non-trivial types never add up to 0, so "-x" cannot be defined for arbitrary categories.