Is there any point in a logician studying $\infty$-categories?

542 Views Asked by At

My primary areas of interest lately have been set theory, logic, and category theory, so naturally topos theory has been a large part of what I'm learning (in between getting caught up on some other things I should really know). I've recently been introduced to the idea of weak Kan complexes and the idea of an "$\infty$-topos". They seem interesting in the sense that I find the formalism pretty, but I don't have a really solid idea for them yet.

As a logician, should I bother to learn more about $\infty$-categories? I gather it's more closely related to the topological end of category theory, but I can't gather from what I can Google whether a logician might have any reason to delve into them.

1

There are 1 best solutions below

5
On BEST ANSWER

I'm not an expert but I'd say that you could really interested in learning about $\infty$-topos theory because of homotopy type theory.

As I said I'm not an expert, I've just started learning this stuff so what follows maybe incorrect, I apologize in advance and thank anyone who will point out any mistaken.

For what I've got so far Homotopy type theory should be the internal language of a $\infty$-topos, pretty much like higher order logic is the internal language of a topos, or simply typed type theory should be the internal language of a cartesian closed category, etc....

Homotopy type theory is a sort of dependent (Martin Löf) type theory with some additional axioms, like the univalence axiom. This kind of type theory is intended to be a type theory in which types should behave like homotopy types of homotopy theory. For this reason such kind of type theory can be interpreted in $\bf SSet$ (the category of simplicial sets) and any other category with enough structure to allow to do homotopy theory.

Anyway as I've said homotopy type theory is not just the language of $\bf SSet$ but the language of $\infty$-topos, so just like we are not limited to interpret a first order language in $\bf Set$, but we can use any topos instead, we can use any $\infty$-topos to interpret homotopy type theory.

So as much one is interested in studying topos theory since they are the environment in which one can interpret HOL, one should also be interested in $\infty$-toposes since they are the categories in which interpret homotopy type theory.

If you interested in more on homotopy type theory you can start reading the book or try to have a look at the homotopy type theory page.