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.
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.