During this seminar, the fellows participating in the CAS project Homotopy Type Theory and Univalent Foundations will introduce themselves and their work, as well as discuss their plans and goals during their one-year stay at CAS. 

Attendence by invitation only.

About the project:

What is a proof? And what does it mean to be equal?

The answers to these questions vary enormously, both through time, but also from one culture to another. The modern mathematical proof may seem the most rigorous of all alternatives. Still, the ideal of well-documented, accountable knowledge, communicated with a proof certificate, is in no way reached. Typically, the validity of extremely complicated mathematical proofs is still supported only by the community's trust in peer review performed by a few acknowledged experts.

Since modern society depends on mathematics, secure foundations are important. In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge. 

In this approach equality has a topological interpretation, yielding great flexibility. Our project aims to further explore this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.

Programme

Monday

09.30-10.30 BJØRN IAN DUNDAS, University of Bergen, & CAMILLA SERCK-HANSSEN, Scientific Director of CAS

• Welcome to the CAS Year on Homotopy Type Theory and Univalent Foundations

10.45-11.45 CHRISTIAN SATTLER, University of Gothenburg

• A Constructive Perspective on Homotopical Algebra Using (Marked) Semisimplicial Sets

12.00-14.00 LUNCH

14.00-15.00 BENEDIKT AHRENS, University of Birmingham

• A Type Theory of Type Theories

15.30-16.30 DANIEL GRAYSON, University of Illinois at Urbana-Champaign

• Some Projects I’d Like to Work On

Tuesday
09.30-10.30 STEFANO PICEGHELLO & KRISTIAN ALFSVÅG, University of Bergen

• Monoidal Structures and Formalization of Coherence Theorems
• The Barratt-Priddy-Quillen Theorem in Homotopy Type Theory

10.45-11.45 ULRIK BUCHHOLTZ, Technical University Darmstadt

• Model Structures on Cubical Sets

12.00-14.00 LUNCH

14.00-15.00 PETER LEFANU LUMSDAINE, Stockholm University

• Towards a General Meta-Theory of Type Theories

15.30-16.30 KUEN-BANG HOU (FAVONIA), University of Minnesota

• TBA

Wednesday
09.30-10.30 FLORIS VAN DOORN, Carnegie Mellon University

• Spectral Sequences in Homotopy Type Theory

10.45-11-45 THIERRY COQUAND, Chalmers / University of Gothenburg

• TBA

12.00-14.00 LUNCH

14.00-15.00 PETER DYBJER, Chalmers / University of Gothenburg

• Internal Type Theory Revisited

15.30-16.30 MARC BEZEM, University of Bergen

• Experiences with Teaching Homotopy Type Theory