Dependent eliminator for empty type in intensional Martin-Löf type theory

Question

In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator.

But let's say I'm setting up intensional Martin-Löf type theory with the primitives $0$, $1$, $2$, $\Pi$, $\Sigma$, $\mathrm{Id}$, $W$ and the universes (like in this pdf).

Do I have to make the eliminator for $0$ dependent or can it just be $\mathrm{absurd}_C$ for each fixed type $C$? Does this choice make any difference (e.g. some type is inhabited if the dependent eliminator is allowed and not otherwise)?

Intuitively it doesn't make sense that the eliminator must be dependent as there is nothing to depend on.

Answer 1

$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\lambda\,x.\,A)\,x$. Also, both types are propositions because of the $0$-s in domains. There's not much reason to assume or use $\text{elim}$ instead of $\text{absurd}$.