Abstract: We will review the notion of model of dependent type theory, with prescribed constructors. Then we will describe work of Kapulkin, Lumsdaine, and Voevodsky producing a model in the category of simplicial sets, for which the Univalence Axiom holds.