CoqHoTT: Coq for Homotopy Type Theory
The goal of this project is to go further in the correspondence between proofs and programs which has allowed in the last 20 years the development of useful proof assistants, such as Coq (developed by Inria). Those assistants have shown their efficiency to prove correctness of important pieces of software but their democratization suffers from a major drawback, the mismatch between equality in mathematics and in type theory (which is the theory at the heart of Coq). Thus, significant Coq developments have only been done by virtuosos playing with advanced concepts of both computer science and mathematics. Recently, an extension of type theory with homotopical concepts has been proposed by field medal Vladimir Voevosdky, which allows for the first time to get the right notion of equality in theorem provers. The main goal of the CoqHoTT project is to provide a new generation of proof assistants based on this fascinating connection between homotopy theory and type theory.
In this talk, I will spend a long time presenting the basics of Type Theory and Homotopy Type Theory and try to present quickly the main goal of the CoqHoTT project.