The monster model and the independence theorem for simple theories Forking independence in simple theories satisfies the 'independence theorem', so does Kim Independence in NSOP$_1$ theories. This theorem is often stated with reference to a monster model. For example, in Tent and Ziegler (condition (f)):1
I am interested in understanding this statement without reference to any underlying monster model, in order to further my intuition.
 A: Here is a restatement of the independence theorem, without the monster model convention. I have been lazy and written $\perp$ in place of the independence anchor symbol.
Let $M$ be a model. For any elementary extension $M\preceq M'$ and $a,a',b,b'\in M'$, if $\mathrm{tp}(a'/M) = \mathrm{tp}(b'/M)$ and $$a\perp^0_M b, a'\perp^0_M a, b'\perp^0_M b,$$ then there exists an elementary extension $M'\preceq M''$ and $c\in M''$ such that $\mathrm{tp}(c/Ma) = \mathrm{tp}(a'/Ma)$, $\mathrm{tp}(c/Mb) = \mathrm{tp}(b'/Mb)$, and $c\perp^0_M ab$.
In general, translating a statement to remove the monster model convention just requires you to specify which model all elements live in. Typically, all you need to do is pair quantifying over elements by quantifying over elementary extensions of the current model. This is what I did in the statement above, moving up from $M$ to $M'$ to $M''$.
This is one way that the monster model convention simplifies bookkeeping in statements and arguments: thanks of saturation, everything that could happen (at least with respect to realizing types over small sets) already happens in the monster model, so we we don't need to keep track of these elementary extensions. The other convenience is that, thanks to strong homogeneity, we can replace cumbersome arguments involving elementary amalgamation with more intuitive arguments involving automorphisms of the monster model. This second convenience doesn't come into play in the statement of the independence theorem - but it certainly does in the proof!
A: Alex Kruckman's answer gives you a direct way to remove the monster model from notation, and makes clear its actual role: just a notational convenience so that we don't have to move to bigger models every time we want to realise some new type or so. There are two alternative intuitions for the independence theorem, one phrased in terms of types and a category-theoretic one.
We will stick with the independence theorem over models, the one over arbitrary sets with respect to Lascar strong types is a bit more complicated. I will write this answer in terms of Kim-independence for NSOP$_1$ theories, which in simple theories is the same as forking-independence (and so the answer applies to that scenario as well). Copying Alex's laziness, I will write $\perp$ for the independence relation.
In terms of types. Let $p(x)$ be some type over a model $M$. Let $M \preceq N$ be an elementary extension and let $b,c \in N$ be tuples. Let $p_1(x, b)$ and $p_2(x, c)$ be extensions of $p(x)$ to parameter sets $Mb$ and $Mc$ respectively. The independence theorem then says that if $b \perp_M c$ then $p_1(x, b) \cup p_2(x, c)$ does not Kim-fork over $M$. So from this point of view, the independence theorem is a statement about amalgamation of types.
A category-theoretic perspective. Suppose we are given a commuting diagram consisting of the solid arrows below, where the objects are models and the arrows are elementary embeddings.

For notational convenience we will assume that these embeddings are genuine inclusions of the underlying sets of the models. Then the independence theorem states that if $A \perp_M B$, $B \perp_M C$ and $C \perp_M A$ then we can complete the diagram by finding a model $N$ together with the dashed elementary embeddings, so that everything commutes and $A \perp_M N_3$. So from this point of view, the independence theorem is a statement about independent amalgamation of models. This formulation is sometimes also called "3-amalgamation".
Both these statements are in fact equivalent to the independence theorem (modulo some basic properties, such as monotonicity and extension). The proof of this for the statement in terms of types is straightforward and amounts to just writing things out. For the categorical statement the proof is less straightforward, although it is considered "standard", and could be considered a question in its own right.
