Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theory $\mathsf{MLTT}{\mathsf{lock}}$ supporting the connectives of standard Martin-L{"o}f Type Theory as well as an S4-style necessity operator. $\mathsf{MLTT}{\mathsf{lock}}$ supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type-checking algorithm for $\mathsf{MLTT}{\mathsf{lock}}$, using a novel extension of normalization-by-evaluation. We have also implemented our algorithm in a prototype proof assistant for $\mathsf{MLTT}{\mathsf{lock}}$, demonstrating the ease of applying our techniques.