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?

]]>