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

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.

-
Do you believe that proof-relevant logic is something logicians should study? – Zhen Lin Nov 19 '13 at 16:08
@ZhenLin: I would have no idea, but it sounds like a thing I'd look into... – Malice Vidrine Nov 19 '13 at 17:35

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.

-
Thanks! Come to think of it, I'd run across the HTT page before when I knew less and simply said "ew, constructive mathematics..." Now I know a bit more and my response is "ew, constructive mathematics; but homotopy..." – Malice Vidrine Nov 21 '13 at 0:45
instead of making a new reference request question, do you know of any non-topologist-friendly intros to simplicial sets you'd recommend? nLab is thorough, but severe, and I'm having a hard time figuring out what a "horn" even is... – Malice Vidrine Nov 22 '13 at 19:40
@MaliceVidrine maybe I've something but I've to search in my list of downloaded preprint. So if you can be a little patient I'll try to take a look :) – Giorgio Mossa Nov 22 '13 at 22:33
Patience is not a problem. Don't go terribly out of your way, but if you run across something it's awful appreciated. – Malice Vidrine Nov 23 '13 at 0:39
Constructive mathematics is actually relevant to mathematicians at large! Who would have thunk it? Also; Topoi are constructive in general: the algebra of open sets of a space is Heyting but not Boolean in general. – cody Feb 27 '14 at 23:12