Many geometric aspects of schemes in different topologies can be seen as consequences of the internal logic of the sheaf topoi on the corresponding sites. For instance, in the Zariski topology on (opposites of) $k$-algebras forces the canonical line object $\operatorname{Spec}k[x]$ is a local fraction ring, and this enriches the synthetic differential geometry of the Zariski topos. The étale topology forces the étale topos to admit a synthetic inverse function theorem, and finer topologies enrich the geometry further in many ways I don't understand.
From this question I leanred the logic of the topos of simplicial sets satisfies the Kreisel-Putnam axiom. Probing a little online I see articles and papers which describe this axiom and its relationship to other types of logic. I would like to know instead what interesting consequences this fact has which are geometric, or at least familiar from algebraic topology and homotopy theory. I have never seen anything about simplicial sets proved internally, nor their internal language mentioned.
What are some geometric implications of the satisfaction of the Kreisel-Putnam axiom in the topos of simplicial sets?
