Till innehåll på sidan

Anders Mörtberg: Cubical techniques in homotopy type theory and univalent foundations

Tid: On 2018-10-03 kl 10.00 - 11.45

Plats: Room 31, building 5 kräftriket, Department of Mathematics, Stockholm University 

Medverkande: Anders Mörtberg (Stockholm University, new group member)

Exportera till kalender

Abstract: In recent years there has been a lot of progress on a variety of problems in homotopy type theory and univalent foundations using cubical techniques. This has for example resulted in multiple constructive justifications to Voevodsky's univalence axiom, new models of higher inductive types and an analysis of the proof theoretic strength of the univalence axiom. Another interesting aspect of these developments is that we can design type theories inspired by these cubical models in which functional extensionality, univalence and higher inductive types are directly definable and hence has computational content. I will give an overview of these developments and discuss some current challenges and open problems.