The Univalence Axiom
In this talk, we will begin by discussing application of functions on paths, and the transport lemma (Lemma 2.3.1 of the book). We will then discuss the notion of homotopies, and equivalences, with a few examples. From their we will be able to define a function which will be called “idtoeqv”. Roughly, this function takes equality of types to equivalence of types. This will allow us to state the univalence axiom. If time permits, we will end with how the various type forming constructions behave in the presence of the higher groupoid structure.
Louis Thrall earned his Ph.D. from the CUNY Graduate Center in 2013. He does research in the area of category theory, algebraic topology. More recently he has developed an interest in Homotopy type theory and computer science.