Type theory is a formal system that was originally intended to describe set-like objects, and which is well-suited to formalizing proofs so that they can be verified by a computer. Recently, it was realized that type theory is intrinsically homotopical, and can be used to reason about spaces and other homotopical categories. Voevodsky introduced an axiom that he calls Univalence, which says roughly that homotopy equivalence and equality agree. This axiom holds for spaces, and makes the theory truly homotopical. This talk will start with an introduction to type theory, will introduce Univalence and give examples of its consequences, and will briefly discuss some recent work on developing the theory of localization in homotopy type theory.