Let $T$ be a first-order theory, let $M$ be a monster model of $T$.
For a set $B\subset M$, let $S_n(B) := M^n/\operatorname{Aut}^T(M)$ be the Stone space of complete $n$-types of $T$ with parameters in set $B$.
View the Stone space of types of $T$ over $B\subset M$ as a simplicial set $S_\bullet:n\mapsto S_{n+1}(B)$. Has this point of view been used in categorical logic ?
Alternatively, a 'type' is another name for an 'orbit', so maybe this space and constructions listed below appeared under another name in group theory when looking at the simplicial space of orbits of a group action on $n$-tuples ?
Using the simplicial space of types, one may view a subset of $M$, or rather its complete diagram, as a map from a representable simplicial set to the simplicial space of types sending an $n$-tuple to its type. Similarly, a 1-type is a map from a representable simplicial set to the décalage (=simplicial path space) of the simplicial space of types. Hence, intuitively, a type is something like a homotopy contracting the set of parameters in the space of types.
Has this point of view been used in categorical logic ?
Alternatively, a 'type' is another name for an 'orbit', so maybe this appeared under another name in group theory when looking at the simplicial space of orbits of a group action on $n$-tuples ?
Let me repeat this observation in more detail with notation.
For a set $A$, let $|A|_\bullet:\Delta^\text{op}\to \mathit{Sets}$ denote the simplicial set represented by $A$, i.e. $|A|_n:=A^{n+1}$. Let $[+1]:\Delta^\text{op}\to\Delta^\text{op}$, $n \mapsto n+1$ be the décalage endomorphism of the category $\Delta$ of finite linear orders, and let $\operatorname{pr}_{1,2,\dotsc}:X_\bullet\circ [+1]\to X_\bullet$ denote the obvious map "forgetting" the new vertex added by $[+1]$.
To give a complete diagram of a subset $A\subset M$ is the same as to give a map of simplicial sets $|A|_\bullet \to S_\bullet(\emptyset)$.
To give a complete 1-type with parameters in $A\subset M$ is the same as to give a factorisation (lifting) of the "parameter set" $|A|_\bullet \to S_\bullet(\emptyset)$ as $$|A|_\bullet \to S_\bullet(\emptyset)\circ [+1] \xrightarrow{\operatorname{pr}_{1,2,\dotsc}} S_\bullet(\emptyset).$$
It is well-known that such a lifting is something like a map from the cone (or perhaps suspension…), or rather the cone taken separately for each connected component. Hence, "intuitively/simplicially", a type over $A\subset M$ is a homotopy contracting $|A|_\bullet$ in $S_\bullet(\emptyset)$.
All these diagram can also be viewed in the category of simplicial topological spaces (or its full subcategory of simplicial profinite sets). Doing so allows to reformulate basic definitions of stability theory.
A type $p(x/A)$ extends to a global type $p(x/M)\supset p(x/A)$ invariant over $B$ iff in $\mathit{sSets}$ it factors as $|A|_\bullet \to S_\bullet(B)\to S_\bullet(\emptyset)$, and in $\mathit{sTop}$ the same means definable.
Here we view a type as a collection of formulas. Recall a type $p(x/A)$ is invariant over $B$ iff for any formula and a tuple $\bar a \subset A$ whether $\phi(x,\bar a)\in p$ or not depends only on $\operatorname{tp}(\bar a/B)$, and is definable over $B$ iff, moreover, $\phi(x,\bar a) \in p$ iff $d_p\phi(\bar a, \bar b)$ holds for each tuple $\bar a\subset A$, for some formula $d_p\phi$ and some tuple $\bar b \subset B$.
Hence, the definition of stability saying "a theory is stable iff each type is definable" says that the simplicial type space fits into some diagram using the simplicial path space and defining something reminiscent of "contracts to each of its point". What does this diagram means for the simplicial space of orbits of a group action ?
