This is a combined question, strictly speaking I am asking three questions concerning, respectively, homotopy type theory, stable homotopy theory and Yetter-Drinfeld modules. But I believe in the present context they can be viewed as a single question.
After a lecture on HoTT by Voevodsky (at TACL 2013 in Nashville) I asked him whether Homotopy Type Theory can be useful for stable homotopy theory. Without much hesitation he replied that HoTT is not really well suited to describe stable phenomena. We never talked after that, and now we will never talk at all, so I still do not know where the main difficulty lies.
Discussing this with several other people (sorry, don't exactly remember with whom) I gradually developed impression that the main difficulty relates to the fact that there seems to be no known good formalism combining constructive type theory and substructural logics, that would lead to some sort of linear type theory. Among possible models one should have triangulated monoidal categories, like stable homotopy category, and it seems not to be known what is the analog of dependent types there.
The first question then is whether what I said above makes any sense, and whether there is any work in this direction.
A situation where one has something like "linear dependent types" is in the context of Yetter-Drinfeld modules over Hopf algebras. Heuristically, the starting point is the fact that in any category $\mathscr C$ with (Cartesian) products every object $X$ has a unique comonoid structure, and the category of comodules over this comonoid is equivalent to the slice $\mathscr C/X$. One could then try to imitate this in (non-Cartesian) monoidal categories, considering comodules over comonoids as variable families over that comonoid. When this comonoid is equipped with a Hopf monoid structure, one can get a "linear" analog of Freyd-Yetter's crossed G-sets.
The second question is then, whether anybody studied features of categories of Yetter-Drinfeld modules over varying Hopf algebras which would resemble either what happens in HoTT or in stable homotopy category.
And the third question comes from the fact that while there are plenty of examples of monoids in stable homotopy categories (ring spectra) I cannot remember any considerations of comonoids or Hopf objects there. Does anybody know some works on this? Or even more simple question (actually fourth, sorry): in unstable homotopy theory one knows that for a, say, topological group $G$ there are certain homotopy categories of $G$-spaces and of spaces over $BG$ which are equivalent. Is there an analog of this fact in stable homotopy theory?
Or maybe Voevodsky had in mind that there seems to be no analog of univalence in the stable context? (Well that was fifth, I certainly must stop here.)
I found only one related question, Are there connections between Homotopy type theory and Grothendieck's theory of motives?, about possible connections between HoTT and motivic homotopy theory. I discovered my pessimistic comment there, remembering that answer by Voevodsky and arguing that motivic homotopy is in a sense even "more linear" than stable homotopy, so it might be even more difficult to relate these two. Anyway.
Best Answer
With respect to the first question, expanding on my comment which pointed out the nLab page dependent linear type theory and the article by Urs Schreiber, 'Quantization via Linear homotopy types', I'd like to pass on some additional relevant commentary by Urs.
There is a way to express linearity for homotopy types, see stable homotopy type. As Simon pointed out in his comment, the category of parametrized spectra is an ∞-topos, indeed a tangent ∞-topos. One can then look to add an axiom to HoTT that makes it the internal language for tangent ∞-toposes. That axiom should be:
there is a pointed type $X_\ast$
the morphism $\Sigma \Omega X_\star \to X_\star$ is an equivalence
So far this makes the ambient category "linear" in the terminology of Schwede's old article on parameterized spectra. One could now continue to add the axioms
If one could add the infinite set of these axioms, that would be Goodwillie's localization for the tangent $\infty$-topos.
There's work in preparation by Mathieu Anel, Eric Finster, and André Joyal along these lines.