3 ms·

> work over an intuitionistic logic Whoops, yes, you are right. That said, a lot of the development of category theory that I'm aware of, is taking place wit

> work over an intuitionistic logic Whoops, yes, you are right. That said, a lot of the development of category theory that I'm aware of, is taking place with set theory. Certainly the two books [1, 2] that I learnt category theory from do. But that was a while back, and it might be the case that this is different now, I have not kept up with this research direction. For example is there a full, unrestricted formalisation of category theory in HoTT? [1] J. Adamek, H. Herrlich, G. E. Strecker, Abstract and Concrete Categories: The Joy of Cats. [2] S. Mac Lane, Categories for the Working Mathematician.

fmap 8y ago
Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally. What I meant specifically is work such as the following: Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664 which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction. > For example is there a full, unrestricted formalisation of category theory in HoTT? You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.

fmap 8y ago

Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally. What I meant specifically is work such as the following: Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664 which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction. > For example is there a full, unrestricted formalisation of category theory in HoTT? You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.