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
$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?
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.
1 to 2 of 2