Centre for Advanced Study

at the Norwegian Academy of Science and Letters

Homotopy Type Theory and Univalent Foundations

Information

Former 2018/2019 Natural Sciences - Medicine - Mathematics

Abstract

Two central questions in the foundations of mathematics are: '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 the 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 at further exploring this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.

Fellows

  • Ahrens, Benedikt
    Assistant Professor University of Birmingham 2018/2019
  • Alfsvåg, Kristian
    PhD Candidate University of Bergen 2018/2019
  • Awodey, Steve
    Professor Carnegie Mellon University 2018/2019
  • Bordg, Anthony
    Postdoctoral Fellow University of Cambridge 2018/2019
  • Buchholtz, Ulrik
    Postdoctoral Fellow Technical University of Darmstadt 2018/2019
  • Coquand, Thierry
    Professor Chalmers University of Technology & University of Gothenburg 2018/2019
  • Dybjer, Peter
    Professor Chalmers University of Technology & University of Gothenburg 2018/2019
  • Grayson, Daniel R.
    Professor Em. University of Illinois at Urbana-Champaign 2018/2019
  • Hou (Favonia), Kuen-Bang
    Assistant Professor University of Minnesota 2018/2019
  • Huber, Simon
    Postdoctoral Fellow University of Gothenburg 2018/2019
  • Joyal, André
    Professor Em. Université du Québec à Montréal 2018/2019
  • Kapulkin, Chris
    Assistant Professor University of Western Ontario 2018/2019
  • Lumsdaine, Peter LeFanu
    Assistant Professor Stockholm University 2018/2019
  • North, Paige
    Assistant Professor Ohio State University 2018/2019
  • Piceghello, Stefano
    PhD Candidate University of Bergen 2018/2019
  • Riehl, Emily
    Assistant Professor Johns Hopkins University 2018/2019
  • Rijke, Egbert
    Postdoctoral Fellow University of Illinois at Urbana-Champaign 2018/2019
  • Sattler, Christian
    Postdoctoral Fellow University of Gothenburg 2018/2019
  • van Doorn, Floris
    Postdoctoral Fellow Carnegie Mellon University 2018/2019

Previous events

News

Group leader

  • Marc Bezem

    Title Professor Institution University of Bergen (UiB) Year at CAS 2018/2019
  • Bjørn Ian Dundas

    Title Professor Institution University of Bergen (UiB) Year at CAS 1993/19952018/2019
LOGO