Ok, let's try to unpack this a bit. Basically we are trying to define a recursor for a very general inductive datatype in a very complex type theory, with dependent types, universes and impredicativity.
As the authors note, this is the most complicated part of the theory itself.
Let's break it down:
The datatype:
The inductive type $K$ itself, is defined within a given universe $\mathsf{U}_\ell$ with certain parameters, denoted as $a :: \alpha$. In the case of $\mathsf{Vect}$ that might be $\forall n:\mathsf{Nat}.\mathsf{U}_0$.
The constructors:
Here we need a positivity restriction for the recursive bits (that refer to $K$ itself) in the types of the constructor, and, because we're in dependent type theory, we don't want later types to depend on the recursive arguments of the constructors.
Because the types of the constructors are the only important bits in the definition of the inductive type, the body of $K$ itself is just $\Sigma_c(\mbox{the type of the constructor $c$})$. But that means that the "name" of $K$ doesn't actually exist! So, instead, within the type of the constructors, the variable $t$ is used, and it's bound by the $\mu$ construct at the top level of the declaration.
For $\mathsf{Vect}_{\mathbb{Z}}$ (integer valued vectors of fixed length), that would be:
$$ \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, \forall tl:t\ n, \forall e:\mathbb{Z}, t\ (S\ n)\} + 0$$
The recursor:
Ok, so this is starting to take shape. The recursor basically takes, for each constructor, a function of the "result" of the recursive calls, and also the arguments of the constructor (which may be of the inductive type itself!) to the output type $C \ldots$
Note that $C$ is a dependent type shape, it needs to be applied to stuff.
Let's leave aside the large elimination $\mathsf{LE}$ case for the moment.
So we need a way to describe the types those recursive calls, and of course the arguments of the constructors themselves. The recursive calls should have arguments of "shape" $C$, but in the position where the inductive arguments were, and with the extra subterm argument. This is accomplished by replacing the $t\ \mbox{something}$ constructor arguments by $C\ \mbox{something}\ \mbox{subterm}$. This is the part denoted as
$$ C\ \pi_i[b, x](u_i x)$$
the result of that call needs to be applied to the term itself, which is the
$$C\ p[b]\ (c\ b) $$
bit. For $\mathsf{Vec}_{\mathbb{Z}}$, letting $\mathsf{Vec} = \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, t\ n\rightarrow\mathbb{Z}\rightarrow t\ (S\ n)\} + 0$, as above, that would give
$$\mathrm{rec}_{\mathsf{Vec}} : \forall C:\forall n:\mathsf{Nat}, \mathsf{Vec}\ n \rightarrow \mathbb{P},\\ C\ 0\ \mathsf{nil}\rightarrow \left(\forall n:\mathsf{Nat}\ z:\mathbb{Z}\ v:\mathsf{Vec}\ n,C\ n\ v\rightarrow C\ (S\ n)\ (\mathsf{cons}\ n\ z\ v)\right)\rightarrow\\ \forall n:\mathsf{Nat}\ v:\mathsf{Vec}, C\ n\ v$$
(that was hard to get right!)
You can see that the arguments of $\mathrm{rec}$ have similar shape to the constructors, with $C$ substituted in the right places with an additional argument.
If $\mathsf{LE}$ holds, it just means you're allowed to replace $\mathbb{P}$ in the above by the more permissive $\mathsf{U_u}$ for some fresh universe.
Let's just finally note that this is all is a pretty standard fare for a system with dependent types and universes, but grokking it does require some familiarity with such systems first, so if the above still seems impenetrable, you might want to make sure you understand the basics of dependently typed elimination, e.g. Bove and Dybjer's Dependent Types at Work.
