Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
It would be nice if the entry were a little more explicit about the slicing theorem
(here)
In the special case that the small -category happens to be a small -groupoid and that is constant on an object , it ought to be true that an explicit form of this equivalence is given in semi-HoTT notation by
This must be an easy theorem in HoTT?
How would you describe from inside ? I don’t get how this is supposed to be done in HoTT.
Edit: Nevermind I haven’t read this properly.
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 just realized that this page doesn’t discuss the functorality of in at all. I had mistakenly thought it took the contravariant functorality implied by .
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.
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 , and for each the relationship between the yoneda embedding and insertion into the free cocompletion is determined by an automorphism of , but not that these automorphisms are natural in .
There has to be a nice way to show these are homotopic, but I’m having a blind spot here.
I have made the section “Functoriality” a subsection (now here) of the “Properties”-section, right after that on the free colimit completion.
Where the - and -notation is used, I have added more explicit pointer to its definition, namely to this Lemma.
1 to 9 of 9