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:

- 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.
- 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)$.
- 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$.
- 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}$
- 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).
- 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 shit. Thus we have an induced functor $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.
- 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