4 ms·

It's actually not very interesting formulation of category theory. You can't express a category of categories, with isomorphic categories considered equal in th

It's actually not very interesting formulation of category theory. You can't express a category of categories, with isomorphic categories considered equal in this way. Partially, this can be worked around if we state that everything important preserves equivalence (i.e. if A ~ A` and B ~ B` A x B ~ A` x B`). Though, if you want to express this in full generality, you will need Homotopy Type Theory. But, all in all, even formulating all this and proving theorems was a good exercise. Good job!

fmap 9y ago
I agree that doing category theory without homotopy type theory is working with one hand tied behind your back, but you have to realize that it is very different from textbook category theory. For instance, in HoTT you will find that the category of U-small categories is not a 1 category; it's a 2 category (since equality of categories is equivalence, not isomorphism). This is correct and gets rid of a lot of confusion surrounding Cat, but it means that you have to deviate from the textbook definitions a lot. There are at least two formalization of HoTT categories if anybody wants to know more. There's one formalization in HoTT Coq and the formalization as part of the unimath project. Both work heavily with precategories as well as categories in order to formulate some textbook notions without changing all the definitions...
xhusshjd 9y ago
> You can't express a category of categories, with isomorphic categories considered equal in this way. Not sure why you think that. It's a straight-forward construction within this framework and even part of the development[1]. [1] https://github.com/jwiegley/category-theory/blob/master/Instance/Cat.v https://github.com/jwiegley/category-theory/blob/master/Inst...
- solomatov 9y ago
  You are right. I didn't notice compose_respects.
solomatov 9y ago
Concerning everything important. It seems, that it's enough for equality to respect only composition. So, basically category of categories is expressible there. But HoTT would give you much more power.

fmap 9y ago

I agree that doing category theory without homotopy type theory is working with one hand tied behind your back, but you have to realize that it is very different from textbook category theory. For instance, in HoTT you will find that the category of U-small categories is not a 1 category; it's a 2 category (since equality of categories is equivalence, not isomorphism). This is correct and gets rid of a lot of confusion surrounding Cat, but it means that you have to deviate from the textbook definitions a lot. There are at least two formalization of HoTT categories if anybody wants to know more. There's one formalization in HoTT Coq and the formalization as part of the unimath project. Both work heavily with precategories as well as categories in order to formulate some textbook notions without changing all the definitions...

xhusshjd 9y ago

> You can't express a category of categories, with isomorphic categories considered equal in this way. Not sure why you think that. It's a straight-forward construction within this framework and even part of the development[1]. [1] https://github.com/jwiegley/category-theory/blob/master/Instance/Cat.v https://github.com/jwiegley/category-theory/blob/master/Inst...

solomatov 9y ago
You are right. I didn't notice compose_respects.

solomatov 9y ago

Concerning everything important. It seems, that it's enough for equality to respect only composition. So, basically category of categories is expressible there. But HoTT would give you much more power.