Write a Blog >>
Mon 20 Jan 2020 16:50 - 17:12 at Maurepas - Homotopy Type Theory and PC chairs' report Chair(s): Floris van Doorn

Homotopy type theory is an extension of type theory that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations of multiple classical results from homotopy theory. However, many proofs are still surprisingly complicated to formalize. One reason for this is the axiomatic treatment of univalence and higher inductive types which complicates synthetic reasoning as many intermediate steps, that could hold simply by computation, require explicit arguments. Cubical type theory offers a solution to this in the form of a new type theory with native support for both univalence and higher inductive types. In this paper we show how the recent cubical extension of Agda can be used to formalize some of the major results of homotopy type theory in a direct and elegant manner.

Slides (slides_black.pdf)621KiB

Mon 20 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

16:50 - 17:56: CPP 2020 - Homotopy Type Theory and PC chairs' report at Maurepas
Chair(s): Floris van DoornUniversity of Pittsburgh
CPP-2020-papers16:50 - 17:12
Anders MörtbergDepartment of Mathematics, Stockholm University, Loïc PujetGallinette Project-Team, Inria
DOI Pre-print Media Attached File Attached
CPP-2020-papers17:12 - 17:34
Fredrik Nordvall ForsbergUniversity of Strathclyde, Chuangjie XuLudwig-Maximilians-Universität München, Neil GhaniUniversity of Strathclyde
DOI Pre-print Media Attached File Attached
CPP-2020-papers17:34 - 17:56
Jasmin BlanchetteVrije Universiteit Amsterdam, Cătălin HriţcuInria Paris
DOI Media Attached File Attached