Homotopy type theory (HoTT) is an interpretation of intensional, constructive type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, constructive type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos. As such it is developing into a new practical foundation for mathematics. In this lecture I will focus on the connection between HoTT and topos theory, motivated by the application to practical formalization issues. E.g. modern proof assistants (Coq, agda) lack quotient types and a clear mathematical denotational semantics. If time permits, I´ll also speak on the various ways of formalizing real numbers in HoTT.