In this master thesis we want to study the newly discovered homotopy type theory, and its models within mathematics. We look at models in simplicial sets, simplicial symmetric monoids, and a new category which could be ...