Determining all the $1$-types of a given theory I'm trying to solve an exercise in my lecture notes. I'm given the following theory of infinitely many disjoint infinite unary predicates:

Let $L_n$ be the language with $n$ unary predicate symbols $P_1, . . . , P_n$. Let $T_n$ be the theory asserting that each $P_i$ is infinite, the $P_i$ are disjoint, and there are infinitely many elements not in any $P_i$, for $i \leq n$. Finally, let $T = \bigcup_n T_n$.

After having proved that both $T_n$ and $T$ are complete, I'm then asked to determine all the $1$-types of $T$, show that
there's a unique 1-type $p_n$ including $P_n(x)$, and a unique type $q$ that is not
one of the $p_n$.
I have no idea how I'd go about determining all the $1$-types, and while I can certainly find a $1$-type $p_n$ including $P_n(x)$ (by setting $p_n = $ tp$_A(a) = \lbrace ϕ(x) : A \models ϕ(a)\rbrace $, where $A$ is some model with $a\in A$ such that $a\in P_n^A$), but I'm not sure how I'd show it's unique.
I know that if If $π : A → B$ is an isomorphism, $a ∈ A$, $b ∈ B$ and $π(a)= b$ that tp$_A(a) = $tp$_B(b)$, so clearly there's only one $p_n$ obtained by taking a set like tp$_A(a) = \lbrace ϕ(x) : A \models ϕ(a)\rbrace $, but I don't know how to show there are no other $1$-types containing $p_n$ (perhaps this will become clearer once I know what all the $1$-types are). I also have no idea how I'd go about finding the $q$ I'm asked for.
I'd really appreciate any help you could offer.
 A: Your reasoning is quite in the right direction.
To show that these types are unique, first note that if $A$ is any model of $T$, then elements of $A$ which are in the same disjoint part realise the same type. Indeed, if $a,b \in P_n^A$ then we may define $σ: Α \to A$ by $σ(a) = b, σ(b)=a, σ(x)=x$ otherwise. It is easy to check that this is an automorphism of $A$, and automorphisms fix types so $tp_A(a) = tp_A(b)$. We can see that any type of this form contains $P_n(x)$, as $A \models P_n(a)$.
So, let p,q be two types that include $P_n(x)$. We may find $M \models T$ which realises both p and q, i.e. $\exists m_1, m_2 \in M$ with $p = tp_M(m_1), q = tp_M(m_2)$. Since both types contain $P_n(x)$, we see that both $m_1$ and $m_2$ lie in $P_n^M$, and so using the above we have $ p =  tp_M(m_1) = tp_M(m_2) = q$. Hence the type containing $P_n(x)$ is unique. (From there, it is relatively straightforward to show that this unique type $p_n$ is also principal, with principal formula $P_n(x)$)
Now if $A \models T$ with $A' = A \setminus \bigcup_{n} P_n^A$ non-empty, then any element $c \in A' $ defines a type different from the $p_n$, since $A \not\models P_n(c)$ for any n, i.e. $P_n(x) \not\in tp_A(c)$. By using automorphisms which swap two elements of $A'$, and a similar argument to the above, we can show that this type is unique, and furthermore it's non principal as it's not realised in all models of T (some models have $A'$ empty, for example $M = ω \times ω$ with $P_n^M = ω \times \{n\}$).
A: First, you should know that in general determining all the 1-types of a given theory is difficult and that there is no automatic recipe to do it.
One particularly useful way to simplify the task is to show that the given theory admits quantifier elimination, that is, that every first-order formula $\phi(x)$ is logically equivalent modulo $T$ to a quantifier-free formula $\psi(x)$. Then understanding a 1-type amounts to understanding the possible quantifier-free formulas that it contains.
Proving quantifier elimination can be done "by hand", by exhibiting a quantifier-free formula for every existential positive formula (i.e., a first-order formula of the form $\exists \bar y(\bigwedge ...)$ where inside the conjunction only atomic formulas appear). Perhaps you can already see how to do this for your example.
Another way to do it is to use properties of the models of $T$ (which is particularly useful when $T$ is $\omega$-categorical for example, since it only has one countable model). For example, if $T$ is $\omega$-categorical, it has quantifier elimination iff its unique countable model is ultrahomogeneous (i.e., every partial isomorphism between finitely generated substructures extends to an automorphism of the whole model). You can for example check that the unique countable model of every $T_n$ is indeed ultrahomogeneous. Even if $T$ is not $\omega$-categorical, this is enough for your purposes: every fo-formula only involves finitely many of the predicates $P_i$, therefore by quantifier-elimination for $T_n$, it is equivalent modulo $T_n$ to a quantifier-free formula. This equivalence is still true modulo $T$, therefore $T$ has quantifier elimination.
