okay so I think I have a satisfying answer to this now...

the bit about BG being a homotopy quotient is a bit of a red herring. If we are thinking in terms of ∞-groupoids, then BG simply *is* G but viewed as a(n) (∞)-groupoid

1/k i guess
idk how long this is gonna go https://twitter.com/schala163/status/1273429627671887872

thinking about *locally trivial* bundles is also a bit of a distraction. If I just give you X as a homotopy type/∞-groupoids, you can't even say what a "locally trivial bundle over X" should *mean*

Don't make me point to the sign:

https://twitter.com/schala163/status/1278474738772443136

2/k

we should really just be talking about fibrations

in general we might wanna be able to say something like "fibrations over X with (homotopy?) fiber F are classified by ___________"

3/k

here F could be all sorts of things. The easiest to think about is if F is just a set (or a really a setoid I guess). But we might also want to allow F to be a higher groupoid in it's own right... later

4/k

Also instead of being "just" a set(oid), F might have some extra structure, e.g. a vector space or some other algebraic gadget...

for G-bundles, we are talking about fibrations of G-spaces where the (homotopy?) fiber is the left(or is right better?) action of G on itself

so I think that what should happen in general is that F-fibrations are classified by maps to the delooping of Aut(F)

umm I'm a little unclear about whether I should be talking about pointed or unpointed stuff here...

6/k

if F is just a set(oid) then Aut(F) is just a group, and it's delooping is a groupoid, and this should recover the classification of (associated bundles of) Aut(F)-principal bundles by maps to B(Aut(F))

7/k

if F is something fancier, say an n-groupoid... then I'm not quite sure but I *think* that makes Aut(F) an n-group and its delooping an (n+1)-groupoid... I definitely need to think about this more lmao

8/k

okay so why should this be true?

well suppose we have a fibration F->E->X

we need to get a map X->BAut(F) from this data

where ofc by "map" I mean "morphism of ∞-groupoids"... I'm a bit confused cuz it *feels like* I want everything to be pointed, so maybe ∞-groups...

9/k

so it turns out I don't actually want X to be pointed... also I need to be more careful with what "Aut(F)" means. I should really be looking at the (∞)-groupoid spanned by everything that's equivalent to F (aka a connected component in the ∞-groupoid of ∞-groupoids LMAO)

10/k

okay so how to describe this morphism of ∞-groupoids given a fibration...

well start by saying what happens to points: a point in x gets mapped to the fiber F_x

11/k

now if I have a path from x to y, I can lift it to a path from each point in F_x to some point in F_y. Not unique, but I think it's close enough that this will give a well-defined *homotopy class* of maps F_x->F_y.

AKA a 1-cell in (the artist formerly known as) BAut(F)

12/k

Then you do the same thing for homotopies between paths and you get 2-cells in BAut(F), and so on for higher cells...

there's a *lot* of coherence to keep track of and details im prolly missing ofc... but like this is *basically* the idea I think

13/k

I think it's nice to compare this (*very* sketchy) sketch to the proof that

[X,BG] classifies principal G-bundles if X is a CW-complex.

the one I know goes by inductively constructing a map X->BG, and the key step boils down to understanding G-bundles over spheres...

14/k

and umm I'm pretty tired and idk if anyone is gonna read this shit lmao... so I maybe won't try to explain this anymore rn

15/k(k=15? unless someone wants to read more idk)