@TimCampion to offer a different point of view, i would regard this as a defining property. namely, one of the fundamental problems that quasicategories address is that homotopy equivalences aren't invertible in the strict sense. the two facts that levelwise equivalences do become invertible in the coherent sense, & that coherent diagrams can be made equivalent to strict diagrams, makes coherent category theory immediately interesting & useful from a classical point of view

so if we didn't have that property, we're back to zigzags of diagrams, or calculus of fractions, or model categories, or some other technical tool to address it in a different way.

@PhilTosteson @RuneHaugseng @S.carmeli @DylanWilson @TylerLawson Thanks! It's neat how many different perspectives there can be on this!

I think what I find confusing is the following. In $Fun(BG,Spaces)$, every object is equivalent to one where the $G$-action is free. But in $Fun(BG, Set)$, this is not the case -- even though $Set$ is a full subcategory of $Spaces$.

I suppose this is because I'm equivocating on what "free" means. But it still feels weird.

well, we could redefine Set so that EG is allowed to be a member

or redefine Spaces to be Kan complexes X such that X_0 -> pi_0(X) is an isomorphism

So, is this proof of Vandiver's conjecture true? arxiv.org/abs/2001.09702

@TimCampion I don't know what you mean by a "free" action. Not every object is equivalent to one such that the homotopy fixed points are empty, for example

In $\mathrm{Fun}(BG,\mathrm{Space})$, $EG$ is actually equivalent to the point with the trivial action, so there's not really a sense in which it is "free" (unless by "free" you mean cofibrant, in which case it becomes obvious that's a model-dependent notion)

@CharlesRezk Wow! Is Vandiver's conjecture the same as the Kummer-Vandiver conjecture? The one equivalent to calculating $K_{4n}(\mathbb Z)$?

@DenisNardin Yeah, I'm not sure what I mean exactly. But it feels weird that in higher category theory we have this distinction between genuine vs Borel equivariance whereas I think the two coincide in ordinary category theory?

@TimCampion I mean, it is a distinction about what maps you invert in your localization. Yeah, it is interesting, but I don't think it's useful to see it as a distinction between 1-categories and ∞-categories

I guess part of what makes it weird to me is that $\infty$-categorically, the construction of $Fun(BG,Spaces)$ doesn't involve a localization.

So it feels strange that for any point-set model, you seem to need to localize.

I mean localize beyond "the most obvious thing"

The most obvious thing will get you genuine stuff

@TimCampion I'm actually unsure of which of the two is "the most obvious"

Maybe that's fair. If I take the 1-category of $G$-spaces and take generating cofibrations to free $G$-cells with the usual interval object, I'll get a model structure for Borel $G$-spaces where the equivalences between cofibrant objects are $G$-homotopy equivalences...

I guess I'm thinking that $G$-homotopy equivalences are the "obvious notion of equivalence"

So from that perspective it comes down to what you think the obvious cofibrations are...