If you know about Lurie's proof of cobordism hypothesis, then I wonder why you're so sceptical. Both the theorem and its proof are based on $(\infty,n)$-categories essentially. Personally I believe TQFTs alone would be enough of a reason to study higher categories.

Pretty much any large enough book on topos theory is bound to describe its connection to topology. A good list of references (of vastly varying difficulty) is at the nLab page. However I believe that topoi are much more connected to logic than to topology.

$A_1$-spaces are classically called H-spaces. It is a theorem that H-spaces are precisely the retractions of $A_\infty$-spaces. Retractions can change your space pretty wildly. For example, a retraction of a finite CW-complex can be not equivalent to a finite CW-complex (see Wall finiteness obstruction). It would be more surprising if $A_1$ and $A_\infty$ happened to coincide.

@AndrejBauer, personally I would be majorly disappointed if the only way to define associative algebras in HoTT were to grind through associahedra. We already have this problem in set theory. Why bother with types if the answer is the same (bar their logical usefulness)? Besides we already have a simple and complete answer in one special case: composition on loop spaces.

@Pete, I doubt that the $\{0,\dots,n-1\}$ definition should be used even at high school level. Personally I was introduced (along with many other students) to the $\mathbb{Z}/n\mathbb{Z}$ definition at the 7th grade, without saying such words as "rings" or "factorsets" of course. It was very simple and we could easily prove some basic properties, like that it is really a ring or a field for prime n. Can't imagine proving anything with another definition.

I would rephrase this in layman's terms as "any function $X\to Y$ is uniquely determined by its pointwise action on elements of $X$, whatever $X$ and $Y$ mean". You know, the basic "a function is a rule which maps each element of $X$ to some element of $Y$". Something that is definitely true in naive set theory but fails miserably in most categories and is problematic in axiomatic set theory. Now the trick is that if you generalize your notion of "element" from a morphism $pt \to X$ to a general $\Gamma \to X$, then the naive definition of function becomes correct - by Yoneda's lemma!

Note that the central extension you're talking about is with Gl (V), not V. This fact is the same as "V-bundles over X equal $ H^1 (X, BGl (V) ) $", which should be familiar.

While your general point of view is valid, it doesn't really offer anything new. Groups and spaces are essentially equivalent objects (modulo some discrepancies), because for any group we can take its delooping (classifying space BG) and it induces an equivalence between groups and connected pointed spaces. Also, while it is possible to choose a group structure on a (homotopy equivalent to the) space of loops (see Kan loop group), it is a very complex and intractable object.

I can reasonably see why functors $BG\to SSet$ should work for discrete groups. I'm not so sure if we start talking about the general ones.

I was talking about Higher Topoi, but HoTT also has relevance. My question stems from it: how do you define G-spaces in HoTT? Even if you shun some obvious problems (like defining categories and actions type-theoretically) the problem remains: HoTT cannot define the standard G-equivariant category, since it identifies equal objects, like equivalent types and homotopic maps (it would imply that $EG$ and $pt$ have the same type of G-structures). Since HoTT is very simplicial-like, the obvious first step would be to know what happens in $SSet$.

Thank you, Tim, I'll take a look at those papers. However, using $G/H \times \Delta^n$ seems just the same as considering simplicial presheaves on orbits. From this PoV the theory doesn't differ from the general HTT nonsense. While fun and useful, it doesn't really explain what a G-space is, simplicially.

If I understand correctly, you are only interested in localic topoi and G-bundles which are locales. If you are using "locale" in a common sense (a Heyting algebra), then I don't see why should you care about $\infty$-topoi. Your question seems to be purely 1-categorical, and is classical as such.