12:59 AM
@CharlesRezk Yes. @MarcHoyois wrote down a nice argument here: mathoverflow.net/questions/130999/…

1:16 AM
Thanks

Using the same sort of argument it is also not difficult to see that the smooth ∞-topos has a conservative family of points given by taking the stalk at the origin in ℝⁿ for each n ≥ 0.

4 hours later…
5:09 AM
@PaulVanKoughnett hah indeed
i'm having a variance issue that i can't sort out.
1. i believe that the "free cocompletion" functor $PShv : Cat \to Pr^L$ should be a 2-functor, with variance as depicted.
2. the functor $PShv$ is the composite
$$Cat \xrightarrow{(-)^{op}} Cat^{2op} \xrightarrow{Fun(-,Spaces)} (Pr^L)^{2op}~,$$
with variance as depicted. here, $Cat \xrightarrow{Fun(-,Spaces)} Pr^L$ is 1-functorial by left Kan extension, and as for 2-morphisms, a morphism $F \xrightarrow{\alpha} G$ in $Fun(A,B)$ determines a morphism $F_! \to G_!$ in $Fun^L(Fun(A,Spaces),Fun(B,Spaces))$.
does anyone see what is going on here?

7 hours later…
12:03 PM
I think that Fun(-,Spaces) should be contravariant on 2-morphisms. Probably easier to see as a composite Cat—->(Pr^R)^{1op}\simeq (Pr^L)^{2op}. (A map of right adjts gives a map the other way on left adjts)

7 hours later…
6:35 PM
Does anyone have any sort of graphical calculus for the six functor formalism? I imagine it might be helpful to have such a thing, especially for reasoning about long strings of compositions of functors, such as in prop 3.6 of Marc's paper arxiv.org/abs/1309.6147
3

4 hours later…
10:43 PM
@BrianShin Very interesting question. Persumably this calculus might be related also to the algebraic structure on the cohomology of groups (like induction restriction and how they behave w.r.t. cup product). I would try to find a graphical calculus for these type of calculations and then try to "categorify" it