A study in Univalence

Abstract

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 called multi pointed simplicial sets. We also describe dependent type theory from the informatical point of view, and some implications of it.