Thursday, December 5, 20137:00 pmHoTT Reading GroupGraduate Center, Room 6417

The Univalence Axiom

Louis Thrall

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.