I spent a lot of the last two years getting really into categorical logic (as in, using category theory to study logic), because I’m really into logic, and category theory seemed to be able to provide cool alternate foundations of mathematics.
Indeed, and ∞-categories can provide semantics of homotopy type theory. But ∞-categories are ultimately based on sets. At some point though maybe we’ll use HoTT to “provide semantics” to set theories, who knows.
In general, there’s a close syntax-semantics relationship between category theory and type theory. I was expecting to touch on that in my next post, though!
EDIT: Just to be clear, type theory is a good alternate foundation, and type theory is the internal language of categories.
Category thing doesn’t. But, (the closely related) homotopy type theory does.
Indeed, and ∞-categories can provide semantics of homotopy type theory. But ∞-categories are ultimately based on sets. At some point though maybe we’ll use HoTT to “provide semantics” to set theories, who knows.
In general, there’s a close syntax-semantics relationship between category theory and type theory. I was expecting to touch on that in my next post, though!
EDIT: Just to be clear, type theory is a good alternate foundation, and type theory is the internal language of categories.