The CoqHoTT Project
Coq for Homotopy Type Theory

ERC Starting Grant (2015-2020)

CoqHoTT in a nutshell

CoqHoTT stands for 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. 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 computer science and mathematics. Recently, an extension of type theory with homotopical concepts has been proposed by Fields medal Vladimir Voevodsky, 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. The impact of the CoqHoTT project may be very strong as it will promote Coq as a major proof assistant, for both computer scientists and mathematicians, as it should become an essential tool for program certification and formalization of mathematics.

The CoqHoTT team


  • The CoqHoTT project has just been accepted by ERC. June 2015-May 2020.
  • Slides of the (very quick) presentation of the project.

Members of the team

Simon Boulier Research Engineer

Gaetan Gilbert PhD Student

Théo Winterhalter PhD Student

Cyprien Mangin PhD Student

Ambroise Lafont PhD Student

Antoine Allioux PhD Student

Eric Finster Post-Doc

Pierre Vial Post-Doc

Matthieu Sozeau Inria Junior Researcher

Nicolas Tabareau Inria Junior Researcher

Past members

Kevin Quirin Teacher in Mathematics

Gabriel Lewertowski Leave for industry

Pierre-Marie Pédrot Inria Junior Researcher

Benedikt Ahrens Birmingham Fellow

Danil Annenkov Post-Doc


Research Topics

  • Define an internalization of Homotopy Type Theory in Coq.
    As witnessed by the outcome of a whole year of work of leading mathematicians and computer scientists of the field (during The Univalent Foundations Program at the Institute for Advanced Study in Princeton [1]), developing a direct complete treatment of homotopy type theory is a very complex task that is far from being accomplished. This is mainly because it raises a lot of coherence issues coming from the use of infinitely many dimensions. We are confident that defining an interpretation of homotopy type theory inside type theory is the key to successfully interpret it. The main challenge is to internalize the definition of the infinite structure involved in homotopy type theory. There are various recent current works on the subject on which we plan to base our investigations. The original model of Voevodsky is based on Kan simplicial sets but suffers from decidability issues (mainly due to degeneracy maps) which does not make it a good candidate for mechanization [2]. The infinite structure could be described using an operadic approach to ∞-groupoids. Indeed, although the usual enriched inductive construction of strict n-categories is known to be broken in the weak setting, Trimble [3] has recently proposed to use specific operads to parametrize the weakly associative composition in the higher-dimensional structures and recover an inductive definition of weak n-categories. Cheng and Leinster [4] have recently propose a co-inductive construction of weak ∞-categories based on Trimble’s approach and on the notion of terminal coalgebras. Another line of work, initiated by Coquand’s team, aims to look at more computational notion of ∞-groupoids, for instance by studying cubical sets [5]. Finally, Altenkirch has proposed to construct ∞-groupoids in a more syntactic way [6], by generating the structure without higher-dimensional coherences and getting back coherences using an “all diagrams commute” approach. It is not clear what is the best description to be used but this question is currently a highly discussed topic among homotopy type theorists.
    • [1] Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program. Institute for Advanced Study.
    • [2] A very short note on the homotopy λ-calculus. Vladimir Voevodsky, 2006.
    • [3] What are ‘fundamental n-groupoids’? Trimble T. seminar at DPMMS, Cambridge, 24 August 1999.
    • [4] Weak ∞-categories via terminal coalgebras. Eugenia Cheng, Tom Leinster. arXiv:1212.5853 [math.CT], 2013.
    • [5] A Model of Type Theory in Cubical Sets. Bezem M., Coquand T., Huber S. (2013).
    • [6] A Syntactical Approach to Weak ∞-Groupoids. Thorsten Altenkirch, Ondrej Rypacek. CSL 2012: 16-30
  • Define and implement a general notion of higher inductive types.
    The goal here is to give a meaning to the newly introduced notion of higher inductive types (HIT). Those objects are at the heart of the formalization of homotopy theory inside a proof assistant. Giving them a computational meaning will allow mathematicians not only to formalize and prove theorems in homotopy theory, but also to use type theory to compute the homotopy groups of complex objects. Indeed, homotopy theorists now face a computational blow up in their work on the classification of topological spaces. This blow up is commonly believed to require the use of a computer to assist mathematicians. But the notion of HIT as also consequences in computer science as it provides a new type former that provides constructors together with (relevant) equalities. For instance, version control systems can be modeled with a HIT where committing and reverting correspond to applying equalities of this HIT [2]. Even if HITs have already been introduced in [1,3], their complete and precise definition is the subject of ongoing research [4]. Indeed, for the moment, existing HITs have been encoded using defined-by-hand axioms to represent elimination rules. This prevents HITs to be defined by non-expert users and also demands to check consistency for each HIT by finding a model in which it can be defined. This situation is clearly not satisfactory but is justified by the fact that developing a general theory for HITs is a very complex task. Using a compilation phase approach, new investigations of the theory will be directly testable by defining a translation into traditional type theory. We believe that this approach will help converging to a satisfactory definition more quickly.
    • [1] Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program. Institute for Advanced Study.
    • [2] Homotopical Patch Theory. Angiuli C., Morehouse E., Licata D. R., and Harper R. ICFP 2014.
    • [3] Inductive Types in Homotopy Type Theory. Awodey S., Gambino N., Sojakova K. LICS 2012.
    • [4] Higher Inductive Types as Homotopy-Initial Algebras. Kristina Sojakova. POPL 2015.
  • Extend homotopy type theory with new logical/computational principles.
    The goal here is to reuse well-known model transformations [3] to enhance HoTT with new logical principles. The challenge is to give a meaning, through separate compilation phases, to axioms often used in mathematics, such as the law of excluded middle or the axiom of dependent choice. As adding new logical principles may have a computational cost and may weaken the extraction mechanism, our plan is to extend HoTT modularly, letting the user choose with which extension to work. Thus, this challenge consists in achieving a high level of modularity in the logical principle governing the type theory of the proof assistant. We have already proven [1] that the forcing transformation (which corresponds to the presheaf construction) enables to enhance the logic of Coq with new constructors such as general unrestricted inductive types (not to be confused with higher inductive types). We plan to apply this technique to other constructions that require the univalence axiom to be correct and in particular to the sheaf construction. This will allow for instance to implement in type theory the so-called Gödel translation from classical logic to intuitionistic logic, giving this way a computational meaning to the law of excluded middle. The structure underlying homotopy type theory is that of ∞-topos recently studied by Jacob Lurie [2]. The main theoretical challenge of this work package will be to make concrete the forcing transformation and the sheaf construction in the setting of ∞-topoi. Indeed, while pre-sheaves and sheaves have already been defined in this setting, the definitions are very abstract and a huge work need to be done to make them sufficiently effective to be implemented using the language of homotopy type theory. For instance, an effective construction of sheaves requires to reformulate sheaves for ∞-topoi using the notion of Lawvere-Tierney topology [3]. One of the main issue will be the definition of the associated sheaf functor in that setting.
    • [1] Extending type theory with Forcing. Jaber G., Sozeau M., Tabareau N. IEEE Symposium on Logic in Computer Science (LICS) 2012, Dubrovnik.
    • [2] Higher Topos Theory. Lurie J. Annals of Mathematics Studies, Princeton University Press, 2009.
    • [3] Sheaves in Geometry and Logic – A first introduction to topos theory. MacLane S., Moerdijk I. Springer Verlag, 1992.

Job Offers

I am pleased to announce the availability of an expert engineer position for the project (click for more information).
  • Expected start: October 2018.
Concerning PhDs, we already have the chance to have many PhD students until 2019. Do not hesitate anyway to contact us if you are interested in the project.

Organized events


The CoqHoTT project has its own blog, intelligently named CoqHoTT-minute (thanks to Éric Tanter for the suggestion).

Where to contact the PI of the project

I am available @

  • Office: B216
    Département Informatique
    École des Mines de Nantes
    4, rue Alfred Kastler
    F - 44307 Nantes cedex 3
  • by phone : +33 (0)2 51 85 82 37 ,
  • by fax +33 (0)

My email :