100, rue des maths 38610 Gières / GPS : 45.193055, 5.772076 / Directeur : Louis Funar

Keyao Peng

Homotopy type theory for mathematicians
Thursday, 28 January, 2021 - 15:30 to 16:30
Résumé : 

Homotopy type can be regarded as the new foundation of maths, replacing the notion of set. We introduce two basic aspects of type: "Spaces as types" in homotopy theory and "Propositions as types" in logic. Then we show some examples of Proof Assistant(LEAN) based on type theory.

Part 1

Institution de l'orateur : 
IF
Thème de recherche : 
Compréhensible
Salle : 
Salle 4/Zoom
logo uga logo cnrs