Homotopy fibers of infinity functors

Question

Let $F: C \to D$ be an infinity functor. Is it true that the homotopy fiber at $y$ can be described as $C \times_D D^{\simeq}_{/y}$? If not, is there a simple formula resembling this one?

Beside the infinity structure, its points are pairs $(x \in C, s: F(x) \to y \text{ equivalence})$.

Models I am using are the following:

1. Infinity categories are thought as quasi-categories, i.e. simplicial sets in which every inner horn can be filled. If also outer horns can be filled, it is an infinity groupoid.
2. The homotopy category of $C$ has vertex of $C$ as objects, and $Hom_{Ho(c)}(x,y) := \pi_0( \{x\} \times_{\Delta^{\{0\}} } Map( \Delta^1, C) \times_{\Delta^{\{1\}}} \{y\}) $. In other words, we take the simplicial set of "maps from x to y" and we take the connected components. This gives a definition of what an equivalence is, namely something that is iso in $Ho(C)$.
3. Given an infinity category $C$, we denote by $C^{\simeq}$ the subsimplicial set spanned by invertible arrows. One can verifies that this is the maximal subgroupoid of $C$.
4. An infinity functor is just a map of simplicial sets; the set of infinity functors $Fun(C,D)$ has a quasi category structure given by $Map(C,D)^{\simeq}$
5. We have a cofibrantly generated model structure on simplicial sets, the Joyal model (see here for a definition https://ncatlab.org/nlab/show/model+structure+on+simplicial+sets).
6. Generally, if one has a finite diagram D, we have an induced model structure on $C^D$ such that $\lim : C^D \to C$ is right Quillen adjoint to $\Delta: C \to C^D$. The structure is such that cofibrations and weak equivalences are levelwise, and fibrations are obviously a sh*t. Thus we have an induced functor $\mathrm{Holim}: Ho(C^D) \to Ho(C)$. Recall that this means holim is computed by taking a fibrant replacement of the diagram in the above model structure, and then taking the ordinary limit.
7. Homotopy fibers are taken in the context of 6. Namely consider a map $f:C \to D$ and an inclusion $i: \{y\} \to D$. The homotopy fiber at $y$ is defined as the homotopy pullback of the diagram given by $i,f$.

Thanks, Andrea

Answer 1

In general the homotopy pullback of the diagram given by $i:\{y\} \to \mathcal{D}$ and $f:\mathcal{C} \to \mathcal{D}$ is given by first replacing $i$ and $f$ by fibrations between fibrant objects (so that the diagram formed by $f$ and $i$ is fibrant in the injective model structure), and then taking the actual pullback. It turns out that specifically for pullback diagram a slightly weaker condition suffices: it is enough to have one of $i,f$ represented by a fibration between fibrant objects and the other just by any map between fibrant objects (this can be deduced, for example, from Proposition 13.1.2 of Hirschhorn's book on model categories and localizations). In the case at hand $\mathcal{C}$ and $\mathcal{D}$ are already fibrant in the Joyal model structure, and so it will suffice to replace $i$ by a fibration. The map $\tilde{i}:\mathcal{D}^{\simeq}_{/y} \to \mathcal{D}$ (obtained by composing the projection $\mathcal{D}^{\simeq}_{/y} \to \mathcal{D}^{\simeq}$ with the inclusion $\mathcal{D}^{\simeq} \subseteq \mathcal{D}$) is a fibration in the Joyal model structure by the following criterion: a map between $\infty$-categories is a categorical fibration if and only if it is an inner fibration and has a certain lifting property for equivalences (see HTT, Corollary 2.4.6.5). On the other hand, the inclusion $\{Id_y\} \to \mathcal{D}^{\simeq}_{/y}$ is an equivalence of $\infty$-categories, and so the map $\tilde{i}$ can be considered as a fibration replacement for $i$. We may now conclude that $\mathcal{C} \times_{\mathcal{D}} \mathcal{D}^{\simeq}_{/y}$ is a model for the homotopy pullback of $i$ and $f$.