Consider the object classifier of the $\infty$-topos of $\infty$-groupoids. For the role it plays in homotopy type theory as the type of types, let’s denote it as $Type = \coprod_{[F]} B Aut(F)$, the coproduct of the automorphism ∞-groups of all (small) homotopy types $[F]$.
Now attempting to imitate the duality between the category of sets and the category of complete atomic Boolean algebras, we might consider the map taking an $\infty$-groupoid $A$ to $[A, Type]$. Similarly to how the internal Boolean algebra structure on $\mathbf{2}$ induces a Boolean algebra structure on $[X, \mathbf{2}]$, for a set $X$, the internal $\infty$-topos structure on $Type$ induces an $\infty$-topos structure on $[A, Type] = \infty-Grpd/A$, the slice $\infty$-topos.
Question: Just as $[X, \mathbf{2}]$ is a special kind of Boolean algebra, being complete and atomic, how can I characterise those $\infty$-toposes of the form $[A, Type]$?
The answer will probably involve Mike Shulman's suggestions to me: having a set of tiny generators and being a Boolean presheaf $\infty$-topos.
Further questions: with such a characterisation in hand, should we expect a duality between such $\infty$-toposes and the $\infty$-topos of $\infty$-groupoids? What would be the equivalent of Stone Space-Boolean algebra duality?
Best Answer
Let $\mathcal{S}$ denote the $\infty$-category of spaces. For any $\infty$-topos $\mathcal{X}$, there is an essentially unique geometric morphism $\pi^{\ast}: \mathcal{S} \rightarrow \mathcal{X}$. The $\infty$-topos $\mathcal{X}$ has the form $\mathcal{S}_{/A}$ if and only if the geometric morphism $\pi^{\ast}$ is etale. This is true if and only if the following three assertions hold:
$(1)$ The functor $\pi^{\ast}$ admits a left adjoint $\pi_{!}$ (equivalently: $\pi^{\ast}$ preserves small limits).
$(2)$ The functor $\pi_{!}$ is conservative (that is, if $\alpha: X \rightarrow Y$ is a morphism in $\mathcal{X}$ for which $\pi_{!}(\alpha)$ is an equivalence, then $\alpha$ is an equivalence).
$(3)$ There is a projection formula $$\pi_{!}( \pi^{\ast} X \times_{ \pi^{\ast} Y } Z ) \simeq X \times_{Y} \pi_{!} Z.$$
The construction $A \mapsto \mathcal{S}_{/A}$ gives a fully faithful embedding from the $\infty$-category of spaces to the $\infty$-category of $\infty$-topoi. However, I wouldn't be inclined to see this as analogous to Stone duality: as you point out, Boolean algebras of the form $[X, \mathbf{2} ]$ are rather special. It's more analogous to the observation that any set can be regarded as a topological space by equipping it with the discrete topology.
To get a closer analogue of Stone duality, note that the $\infty$-category of $\infty$-topoi admits small limits. Consequently, the functor $A \mapsto \mathcal{S}_{/A}$ extends formally to a functor $F$ from Pro-spaces to $\infty$-topoi which commutes with filtered inverse limits. This functor $F$ is not fully faithful, but it is fully faithful when restricted to profinite spaces (that is, Pro-spaces which can be represented by filtered diagrams of spaces which have only finitely many homotopy groups, each of which is required to be finite). You therefore get an embedding $\theta:$ { Profinite spaces } $\hookrightarrow$ { $\infty$-topoi } which is a better analogue of Stone duality. In fact, it generalizes Stone duality: the RHS contains the ordinary category of sober topological spaces as a full subcategory, the LHS contains the ordinary category profinite sets as a full subcategory, and on the latter subcategory $\theta$ restricts to the usual fully faithful embedding { Profinite sets } $\simeq$ { Stone Spaces } $\hookrightarrow$ {sober topological spaces}.