I have made the section “Functoriality” a subsection (now here) of the “Properties”-section, right after that on the free colimit completion.

Where the ${(\text{-})}^{ladj}$- and ${(\text{-})}^{radj}$-notation is used, I have added more explicit pointer to its definition, namely to this Lemma.

]]>Okay, I’ve finished off the proof. No more gaps, I hope.

This exercise in lining up the details has been a lot more complicated than I thought it would be.

]]>No, I’ve still made an error; I’ve shown that there is a natural equivalence between the free cocompletion and the local left adjoint to $Fun(-, \infty Gpd)$, and for each $S$ the relationship between the yoneda embedding and insertion into the free cocompletion is determined by an automorphism of $S$, but not that these automorphisms are natural in $S$.

There has to be a nice way to show these are homotopic, but I’m having a blind spot here.

]]>I’ve written the promised section on functorality. I think I’ve filled the gaps in my proof that free cocompletion is the local left adjoint to $Fun(-, \infty Grpd)$, by reducing it to the question of automorphisms of $\infty Cat$.

]]>I just realized that this page doesn’t discuss the functorality of $PSh(C)$ in $C$ at all. I had mistakenly thought it took the contravariant functorality implied by $Fun(-, \infty Gpd)$.

So I’ve removed my remark about functorality, since it doesn’t make sense in context. Instead, a new section about functorality should probably be created. I’ll work on that tomorrow.

]]>There are gaps in my argument (and in the resulting exposition) so I’ve reverted. But I’ve saved the contents here in case it can be salvaged.

There _is_ a covariant functor with the same values on objects as $PSh$ that makes this a natural equivalence, namely the "free completion under small colimits" functor. This is, in fact, the [[adjoint (infinity,1)-functor#category_of_adjunctions | local left adjoint ]] to $PSh$, as can be observed by rewriting the equivalence in terms of right adjoints.
If $D$ is a [[presentable (∞,1)-category]], let $Func^R(D, PSh(C)) \subseteq Func(D, PSh(C))$ be the full subcategory of accessible functors that preserve limits (i.e. functors that are right adjoints). Then
+-- {: .un_lemma}
###### Lemma
There is an [[equivalence of quasi-categories]], natural
in small (∞,1)-categories $C$ and
presentable (∞,1)-categories $D$
$$
Func^R(D, PSh(C))^{op} \to Func(C, D)
$$
=--
+-- {: .proof}
###### Proof
Taking an exponential transpose, we can identify
$Func^R(D, PSh(C)) \subseteq \Func(D \times C^{op}, \infty Gpd)$ as the full subcategory of functors $F$
such that every $F(-, c)$ is accessible and preserves limits. Thus, we can compute natural equivalences
$$
Func^R(D, PSh(C))^{op}
\simeq Fun(C^{op}, Func^R(D, \infty Gpd))^{op}
\simeq Fun(C, Func^L(\infty Gpd, D))
\simeq Fun(C, D)
$$
=--

]]>
I expanded on the observation that $PSh(C)$ is the free cocompletion of $C$ by proving that $PSh(C)$ is the local right adjoint to the free cocompletion functor.

]]>How would you describe $\mathrm{PSh}_\infty(\mathcal{C})$ from inside $\mathcal{C}$? I don’t get how this is supposed to be done in HoTT.

Edit: Nevermind I haven’t read this properly.

]]>It would be nice if the entry were a little more explicit about the slicing theorem

$PSh_\infty(\mathcal{C}_{/p}) \stackrel{\simeq}{\to} PSh_\infty(\mathcal{C})_{/y p} \,.$(here)

In the special case that the small $\infty$-category $\mathcal{C}$ happens to be a small $\infty$-groupoid and that $p$ is constant on an object $X \in \mathcal{C}$, it ought to be true that an explicit form of this equivalence is given in semi-HoTT notation by

$\left( (c \overset{\gamma}{\to}X) \;\mapsto\; \mathcal{F}(\gamma) \right) \;\mapsto\; \left( c \;\mapsto\; \array{ \underset{c \underset{\gamma}{\to}X}{\sum} \mathcal{F}(\gamma) \\ \downarrow \\ \underset{c \underset{\gamma}{\to}X}{\sum} \ast } \right) \,.$This must be an easy theorem in HoTT?

]]>