How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?
Dependency is interesting because of equality, and equality is adjoint to contraction. As a result, substructural calculi (which in general omit contraction) do not have an obvious notion of equality.

In type-theoretic language, equality is characterized by the following inference rule[*] being valid in both directions (top-to-bottom and bottom-to-top):

$$
\begin{array}{l}
\Gamma, x:\tau, y:\tau \;|\; \Theta, x = y : \tau \vdash P \\
\hline
\Gamma, z:\tau \;|\; [z/x,z/y]\Theta : \tau \vdash [z/x,z/y]P \\
\end{array}
$$

This says that if you have two free variables $x$ and $y$, and an assumption they are equal, that lets you derive the same things are replacing them both by a variable $z$. Note that going from top to bottom is a contraction -- the number of uses of $z$ will be the sum of the uses of $x$ and $y$. 

As a result, interpreting the meaning of equality in linear calculi is tricky. The obvious thing to do is to restrict your attention to types which are contractible, but it turns out there are multiple incomparable ways of doing so! 

One idea, originating in the work on Linear LF by Cervesato and Pfenning, is to only permit dependency on exponential types. 

I, with Nick Benton and Pierre Pradic, gave another calculus based on another version of this idea, which exploited Benton and Wadler's characterization of linear logic in terms of an adjunction between a cartesian closed category and a monoidal closed category. Basically, we just made the CCC part dependent, so that linear types could be dependent on intuitionistic types, but not vice-versa. (However, you could be dependent on closed linear terms, since they are duplicable.) 

In his PhD thesis, Matthijs Vákár gave a denotational model of Linear LF. His semantics was based on Benton-Wadler adjoint models, so it should also interpret our calculus.

The other main idea is due to Conor McBride, with subsequent refinements by Bob Atkey. His idea is based on resource interpretations of linear logic, with the idea that if you forget the resource usage information on a linear term, you are left with a nonlinear term approximating it. Then, you can depend on that nonlinear term.   

[*] This inference rule is for the case of first-order logic. The dependent case is more complicated, but the underlying issues are the same.