For the definition of a type, can we use an arbitrary complete, satisfiable theory as a starting point?
I'm looking at Marker's definition and wondering why we're insisting on the presence of $M$ in the beginning, since we don't insist that there exist a valuation $\vec{v}$ such that $M, \vec{v} \models p(\vec{v})$.
Here's the definition of an $n$-type, paraphrased for Marker's Model Theory: An Introduction, definition 4.1.1 on page 115.
Let $L$ be a language.
Let $M$ be an $L$-structure.
Let $A$ be a set such that $A \subset M$.
$L_A$ is a language extended with fresh constant symbols for each $A$.
$M$ is additionally an $L_A$ structure, with each new constant symbol interpreted as the element of the domain of $M$ associated with it.
Let $\text{Th}_A(M)$ be the set of all $L_A$ sentences that are true in $M$.
Suppose $p$ is a subset of $L_A$-formulas with free vars $\vec{v}$.
$p$ is an $n$-type if and only if $p \cup \text{Th}_A(M)$ is finitely satisfiable.
(Marker originally used "satisfiable" in the definition, but remarked that we could use "finitely satisfiable" by compactness. I'm choosing to use "finitely satisfiable" in the definition here. For me, at least, explicitly using "finitely satisfiable" really drives the point home that we could be leaving our original structure $M$ when assessing satisfiability.)
$p$ is a complete type if and only if $\varphi \in p$ or $\lnot \varphi \in p$.
We made some stylistic choices when picking this definition.
For example, I think we could also say that a complete $n$-type is maximal among $n$-types w.r.t. inclusion and define it that way.
One choice I'm wondering about is the initial setup, right at the beginning, where we picked $L$ and $M$ and $A$ and then used it to build a theory $\text{Th}_A(M)$.
I'm wondering if we could have instead started with any complete, satisfiable theory $T$ instead of applying this process to create one ... or if that would give us a notion that is inequivalent to a type or is bad for some other reason.