There are two ways of looking at the semantics of type theory.
One tries to stick as closely as possible to the syntax. Put simply, we require just enough mathematical structure to 'interpret the rules' of type theory. This amounts to expressing Martin-Loef type theory as a generalized algebraic theory, i.e. seeing the rules of type theory as certain algebraic operators. There are many equivalent ways of stating this kind of model, including categories with families (CwFs), categories with attributes, etc. The resulting notion of model is what we call strict: it requires a number of on-the-nose equalities between the algebraic constructors, which derive from the equational theory of MLTT.
The other one is to think of type theory more through its universal mathematical properties, and its categorical structure. This begins from Seely's interpretation of type theory in locally cartesian closed categories (LCCCs). These models are less verbose, because a number of constructions follow from the universal properties. However, they are very weak: many of the equalities that type theory postulates strictly are only available up to isomorphism.
While the first notion of model is the 'real' one, the second notion is much closer to mathematics. The objective of strictification theorems* is to construct a model of the first kind (i.e. one close to syntax) from the second kind (i.e. one close to mathematics).
Broadly speaking, there are due strictification theorems for MLTT: one due to Hofmann, and one due to Lumsdaine and Warren. Both have a long pre-history in the 1960s.
Hofmann, Martin. 1995. ‘On the Interpretation of Type Theory in Locally Cartesian Closed Categories’. In Computer Science Logic: 8th Workshop, CSL ’94, Kazimierz, Poland, September 25 - 30, 1994. Selected Papers, edited by Leszek Pacholski and Jerzy Tiuryn, 427–441. Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/BFb0022273.
@inproceedings{hofmann_interpretation_1995,
title = {On the interpretation of type theory in locally cartesian closed categories},
doi = {10.1007/BFb0022273},
booktitle = {Computer {Science} {Logic}: 8th {Workshop}, {CSL} '94, {Kazimierz}, {Poland}, {September} 25 - 30, 1994. {Selected} {Papers}},
publisher = {Springer-Verlag Berlin Heidelberg},
author = {Hofmann, Martin},
editor = {Pacholski, Leszek and Tiuryn, Jerzy},
year = {1995},
pages = {427--441}
}
Lumsdaine, Peter Lefanu, and Michael A Warren. 2015. ‘The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories’. ACM Transactions on Computational Logic 16 (3). https://doi.org/10.1145/2754931.
@article{lumsdaine_local_2015,
title = {The {Local} {Universes} {Model}: {An} {Overlooked} {Coherence} {Construction} for {Dependent} {Type} {Theories}},
volume = {16},
issn = {15293785},
doi = {10.1145/2754931},
number = {3},
journal = {ACM Transactions on Computational Logic},
author = {Lumsdaine, Peter Lefanu and Warren, Michael A},
year = {2015},
eprint = {1411.1736}
}