How to derive dependently typed eliminators?

Question

In dependently-typed programming, there are two main ways of decomposing data and performing recursion:

• Dependent pattern matching: function definitions are given as multiple clauses. Unification ensures that all omitted cases are impossible, and an external solver ensures that recursion is well-founded.
• Eliminators: Each inductive datatype $D$ has an associated constant $E_D$, which acts as an induction principle, and as recursive function that decomposes values of type $D$. These are more verbose, but have the advantage of being total (all cases are covered by $E_D$) and terminating by construction.

I've seen eliminators for common datatypes, like $Nat$, where the eliminator is basically mathematical induction, or $List$, where the eliminator is basically a fold.

I've been reading several papers on dependent pattern matching, and many refer to type theories in which datatypes can be defined, and eliminators are provided by the theory. For example, Eliminating Dependent Pattern Matching describes how UTT is based on eliminators, and how pattern matching can be converted to elimination in the presence of axiom $K$. My understanding is that, once a datatype is defined, the theory provides the eliminator.

What I haven't found (or at least, haven't recognized if I've seen it) is a good description of how one can derive the eliminators, both their types and their semantics.

Can someone point me to a reference that describes how one can obtain an eliminator from the definition of a datatype?