Current proof assistants like Coq and Agda are fairly good for formalizing univalent foundations, and especially with all the work that the Coq people have put in this year, it’s getting better at a fairly rapid clip. However, these programs also have certain limitations that seem hard to get around without redesigning them from the ground up. Thus, it’s worth thinking about what the ideal proof assistant for homotopy type theory would look like, if we were to design one ourselves.
Obviously, there won’t be complete agreement on what features we want. Vladimir has one detailed proposal, which Dan Grayson is already working on implementing. Other people would prefer to keep decidability of type-checking, but include a different set of features. This page is intended as a central place to record all “wish list” features that we might want to have in a proof assistant for univalent foundations, to spur discussion and as a reference for anyone who might be designing such a thing.
Please add your own wishes to the list, and put comments or discussion on what’s already here.
It seems non-negotiable that we need dependent types, dependent sums and products, identity types, and more general inductive types.
Definitional eta conversion for dependent product types is very convenient, and seems to be satisfied in most models. Eta conversion for dependent sums, which is lacking from Coq, can also be very convenient when working with more complicated structures. Agda has a separate notion of “record” which has definitional eta conversion.
Vladimir’s type system also has stronger eta rules for other inductive types, such as the natural numbers, which make type-checking undecidable.
At least HITs with 0- and 1-constructors, and definitional computation rules for 0-constructors. If we can find a good way to implement definitional computation rules for 1-constructors, that would be a bonus. Allowing 2-constructors and so on would also be extra nice.
Since the higher inductive interval with definitional 0-computation rules implies function extensionality, our type theory would then automatically incorporate that principle.
Coq’s inductive types are implemented using separate “match” and “fix” constructions, which allow for deep matching, mutual matching, etc. Similarly, Agda allows function definition by pattern matching with a separate termination checker. However, this approach is only justified semantically by translating it into eliminators, and it is hard to make sense of for higher inductive types. On the other hand, deep matching is very useful for functional programmers.
One potential solution to this problem is the approach used in Epigram, where there is a “pattern matching” syntax that is extensible rather than baked into the system. Any term whose type has “the form of an induction principle” can be used to justify a pattern-matching syntax. Thus, although each inductive definition comes with its defining induction principle, the user can prove their own new induction principles (such as for deep matching, mutual recursion, etc.) and then use those elimination rules with the same sort of pattern-matching syntax.
This may be especially nice for higher inductive types, where preliminary experiments suggest that there can be meaningful notions of “deep recursion” and “mutual recursion” in particular cases, but it seems difficult to give one general formulation of such principles.
We need some sort of universe polymorphism that is more flexible than Coq 8.4 and earlier. Options include the Harper-Pollack algorithm which Mathieu has now implemented in Coq, a system like Agda’s with an internal type of universe levels, or Vladimir’s proposed system.
Since we don’t yet know how to make computational sense of univalence in arbitrary dimensions, probably we will still have to assert univalence as an axiom of some sort.
One may or may not want these. It would be nice to have the flexibility to allow the user to impose resizing-type rules if they so desire.
There are various things one might mean by “reflection”, but one thing is that it would be nice to be able to prove theorems about “all record types” or even “all inductive types”. As it is, if we prove a theorem characterizing, say, what paths in a Sigma-type look like, then that theorem doesn’t apply to a dependent record type even if it is isomorphic to a Sigma-type. This is problematic since for large-scale modular developments, named record types are essential. This might be doable by implementing the whole thing inside a powerful logical framework language, but it might also be possible to internalize the whole thing.
Singleton types, a la Harper-Stone, give a flexible way to include definitions in contexts, and specialize only certain fields of record types.
There seem to be advantages both to a tactic language like Coq’s and to an interactive term-building system like Agda’s. Perhaps one could get the best of both worlds with an interactive mode during which which the user could choose (locally, i.e. at each hole) whether the source file ends up containing the generated term or the tactic calls which generate it. An abstract type for tactics in Coq Tactics in agda
For real-world usability, one would of course eventually want things that serve the purposes of modules, typeclasses, notations, etc. Unification hints allow one to easily implement both canonical structures and type classes. Coq’s module system is not first class and seems way too complicated. The agda module system in mean and lean. O’Connor on modules
It would be awesome if we could draw pasting diagrams and string diagrams in the proof assistant!