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
News
 The CoqHoTT project has just been accepted by ERC. June
2015May 2020.
 Slides of the (very quick) presentation of the project.
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 ncategories 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
higherdimensional structures and recover an inductive definition of
weak ncategories. Cheng and Leinster [4] have recently propose a
coinductive 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
higherdimensional 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 ngroupoids’? 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: 1630
 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 definedbyhand axioms to represent
elimination rules. This prevents HITs to be defined by nonexpert
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 HomotopyInitial Algebras. Kristina
Sojakova. POPL 2015.
 Extend homotopy type theory with new
logical/computational principles.
The goal here is to reuse
wellknown 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 socalled 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 presheaves 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 LawvereTierney 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
We already have the chance to have many PhD students and PostDocs
starting between September 2015 ad May 2016.
Do not hesitate anyway to contact us if you are interested in the project.