I am reading Bierman & de Paiva's paper on intuitionistic modal logic. They offer a typed version on page 401. I wonder whether the result generalizes to $\Sigma$- and $+$-types in Martin-Löf type theory. In particular, I wonder whether the T-rule $\Box A\rightarrow A$ generalizes to the two mentioned types. In other words, can we have the following rules?
$$\Box (A+B)\rightarrow (A+B),\quad\quad\quad\Box\Sigma x:A.B(x)\rightarrow\Sigma x:A.B(x).$$
There's quite a bit of research on modalities in type theory, but I'm uncertain what exactly what you're looking for.
I think some of the oldest stuff would be by Frank Pfenning and Rowan Davies. I believe they develop modal type theory with a view toward staged computataion, where $\square A$ is like an internal classification of closed terms of type $A$. I'm not sure if any of their work has $Σ$ and $+$ specifically, but once that is your mindset, it's not much of a surprise that $\square A → A$ works for them (you get an $A$ value by actually reducing the $\square A$ term).
If you're looking to read about modal type theory from the ground up, I'd look into their work, because it's probably the simplest to start with. A Judgmental Reconstruction of Modal Logic might be a good precursor. A Modal Analysis of Staged Computation should get into some of the ideas I was talking about above. I'm afraid I'm not familiar with all their work on the subject, so there might be additional/better papers I'm not aware of.
If you merely want to see something like MLTT with modalities, I found this. It uses a different presentation, though, and looks quite a bit more complex. Of course, some of that complexity is due to questions that necessarily arise with dependent types and modalities (like, how should equality/identity act for values of modal type). If you get really interested in modal type theory, there is also this which seems like a pretty comprehensive treatment of certain sorts of modal type theories (unfortunately, 'modality', is a vague enough term that it's impossible to concretely describe a generalized framework encompassing modal theories; also unfortunately, I haven't gotten around to reading it thoroughly yet, but it seems great).
Hopefully that's enough to get you started.