André Joyal Homotopy type theory: a new bridge between logic, category theory and topology. b

Talk given on Friday October 26, 2018 in the Graduate Center, CUNY. Résumé: MartinLôf type theory is a language for constructive mathematics with applications to program verifications and proof assistants. The homotopy interpretation of MartinLôf type theory, discovered by Voevodsky and independantly by Awodey and Warren, has initiated a project for a new foundation of constructive mathematics and of homotopy theory. An elementary notion of higher topos is emerging in the process. We shall describe the v