Russell proposed type theory in the first decades of the 20th century in response to the foundational crisis faced by set theory. Over the last century, there have been a number of developments in type theory, in particular the mechanization of type theory exemplified in tools like Isabelle, Coq, and Agda. There have been some notable successes of mechanization both in the field of mathematics (the proof of Kepler’s conjecture) and in computer science (a formally verified compiler, CompCert).

Over the last decade, a new variant of type theory--homotopy type theory (HoTT)--has come to the forefront, providing fine-grained analysis of one of the most important and subtle aspects of logic: equality. It achieves this by importing concepts from homotopy theory. The double payoff is in the new perspectives it provides: for mathematicians, the computational and constructive aspects of type theory; and for computer scientists, the ability to automate and simplify reasoning about equality.

The current paper explains the implementation of a variant of HoTT--cubical HoTT--that minimizes axioms in the theory by introducing an “interval type.” The interval type allows expressing and reasoning about homotopy between functions, directly in the theory instead of the meta-theory, thereby providing a more efficient mechanization of the theory. The paper also shows how features indispensable for a proof assistant, such as pattern matching, can be incorporated in the presence of HoTT constructs such as higher inductive types. The end result is a fully fledged proof assistant for HoTT.

HoTT has generated quite a bit of excitement in foundational maths and in computer science (CS). I am reminded of the situation in the last two decades of the 20th century: monads and their application to programming language semantics--that too was a result of importing some fundamental structures from mathematics into CS, with a deep and lasting impact on the practice of CS. Some of the applications from the formalization of HoTT in Agda are quite exciting; for example, a mechanization of the mathematics of “patches” mentioned in the future work section is intriguing!

I also expect to see HoTT applied to program specification and refinement. The difference this time around--in comparison with monads--is that HoTT will hopefully also have a deep and lasting impact on the practice of mathematics: Agda and other similar mechanizations of HoTT could provide nontrivial assistance to mathematicians in their day-to-day work, as well as make cutting-edge mathematics more accessible by encapsulating it into shrink-wrapped software.