Homotopy Theory and Constructive Mathematics

Abstract: Constructive mathematicians and computer scientists have long been interested in logical theories in which all mathematical statements have computational content. In such systems, any proof of the existence of some natural number automatically gives an algorithm for computing the number. Most modern computer "proof assistants", that is, programs aimed at helping the user construct and verify the correctness of mathematical statements, are based on a class of such systems call *type theories*.

Around 15 years ago, however, it was discovered that the way type theories represent equality meant that, rather than describing constructive *sets*, these systems should more properly be thought of as describing constructive *homotopy types*. This has led to a number of new connections between homotopy theory, higher category theory, computer science and logic. In this talk, I will describe some of these ideas and the results that they have led to.

algebraic geometryanalysis of PDEsalgebraic topologycomplex variablesdifferential geometrygeneral topologygeometric topologyK-theory and homologymetric geometrysymplectic geometry

Audience: researchers in the topic

---

CRM - Séminaire du CIRGET / Géométrie et Topologie

Series comments: Hybrid seminar of geometry and topology. Laboratory : CIRGET - www.cirget.uqam.ca The homepage of the seminar is www.cirget.uqam.ca/fr/seminaires.html

[[Please leave your micro off when entering the seminar room and provide your family name and first name in order to be identified by the speaker.]]

The livestream is on Zoom at : uqam.zoom.us/j/98999725241 (no password is needed).

The recorded talks can be found at CIRGET channel : www.youtube.com/channel/UCLkFm-uEvXSf9y-iQtWOLWA

---