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.
1 to 9 of 9
It would be nice if the entry were a little more explicit about the slicing theorem
PShβ(π/p)ββPShβ(π)/yp.(here)
In the special case that the small β-category π happens to be a small β-groupoid and that p is constant on an object Xβπ, it ought to be true that an explicit form of this equivalence is given in semi-HoTT notation by
((cΞ³βX)β¦β±(Ξ³))β¦(cβ¦βcβΞ³Xβ±(Ξ³)ββcβΞ³X*).This must be an easy theorem in HoTT?
How would you describe PShβ(π) 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 PSh(C) in C at all. I had mistakenly thought it took the contravariant functorality implied by Fun(β,β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.
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(β,β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 have made the section βFunctorialityβ a subsection (now here) of the βPropertiesβ-section, right after that on the free colimit completion.
Where the (-)ladj- and (-)radj-notation is used, I have added more explicit pointer to its definition, namely to this Lemma.
1 to 9 of 9