Definition of $Fun^G( \mathcal C, \mathcal D)$ in the setting of quasicategories

Question

Our research group is currently going through the paper by Thomas Nikolaus and Peter Scholze On Topological Cyclic Homology and in the Appendix B, Proposition B.5., they use the notation $Fun^{B \mathbb Z}( \mathcal C, \mathcal D)$ for the $\infty-$category of $B \mathbb Z$-equivariant functors between two $\infty-$categories $\mathcal C, \mathcal D$ with $B \mathbb Z$ action. The notation hasn't been defined before, at least we couldn't find a definition, and a quick look at Lurie's HHT didn't give anything either.

My assumption is that for a simplicial group $G$ we can define $Fun^{G}( \mathcal C, \mathcal D)$ as a full subcategory of $Fun(BG,Fun( \mathcal C, \mathcal D))$. Two major properties that are used are:

1. There is a natural map (isomorphism?) $ Fun ( C / G , \mathcal D) \rightarrow Fun^G ( C , \mathcal D) $ for $\mathcal D$ having a trivial $G$ action and
2. $Fun^G ( pt , \mathcal D) \cong Fun ( BG , \mathcal D) $. This would follow from 1 if we do have an isomorphism and $Fun^G$ were invariant under homotopy equivalences, since $pt \simeq EG$ and $EG / G = BG$.

Answer 1

A(n ∞-)category with $G$-action is just a functor $BG\to \mathrm{Cat}_∞$. Then, if $\mathcal{C},\mathcal{D}$ are (∞-)categories with $G$-action, we can get another (∞-)category with $G$ action $\mathrm{Fun}(\mathcal{C},\mathcal{D})$ by pairing them: $$\mathrm{Fun}(\mathcal{C},\mathcal{D}):BG\xrightarrow{(i,1)}BG^{op}\times BG\to \mathrm{Cat}_∞^{op}\times\mathrm{Cat}_∞\xrightarrow{\mathrm{Fun}(-,-)}\mathrm{Cat}_∞$$ where $i$ is the functor induced by the group antihomomorphism sending $g$ to $g^{-1}$. This is just the classical functor category equipped with the conjugation action sending $F$ to $gFg^{-1}$.

Then, to get $G$-equivariant functors all you have to do is take homotopy fixed points (i.e the limit of the functor $BG\to\mathrm{Cat}_∞$ ): $$\mathrm{Fun}^G(\mathcal{C},\mathcal{D}):=\mathrm{Fun}(\mathcal{C},\mathcal{D})^{hG}\,.$$ So, morally, $G$-equivariant functors are just functors equipped with equivalences $F\to gFg^{-1}$ and all higher coherences needed. In fact you could spell out explicitely what the higher coherences are, but I'm uncertain this is at all useful in practice.

Let us see a bit how to get the two properties you are interested in.

Note that when they write $\mathcal{C}/G$ they probably mean the homotopy orbits, what's usually denoted $\mathcal{C}_{hG}$, i.e. the colimit of the functor $\mathcal{C}:BG\to \mathrm{Cat}_∞$. Then the first property is just the fact that $$\mathrm{Fun}(-,\mathcal{D}):\mathrm{Cat}_∞^{op}→\mathrm{Cat}_∞$$ commutes with limits. This is true because it is a right adjoint (in fact its own right adjoint, because adjunctions for controvariant functors are confusing).

Finally, the second statement follows from the first as you imagine, e.g. by using the description of colimits in $\mathrm{Cat}_∞$ in Higher Topos Theory, section 3.3.4 to show that $*_{hG}\cong BG$

Remark that everything we did respects equivalences pretty much by definition. In fact the language is cooked up so that we cannot say statements that are not invariant under equivalences.