jaycech3n / isabelle-hott

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Isabelle/HoTT

Isabelle/HoTT is an experimental implementation of homotopy type theory in the Isabelle interactive theorem prover. It largely follows the development of the theory in the Homotopy Type Theory book, but aims to be general enough to eventually support cubical and other kinds of homotopy type theories.

Work is slowly ongoing to develop the logic into a fully-featured proof environment in which one can formulate and prove mathematical statements, in the style of the univalent foundations school. While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL. Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure.

Caveat prover: This project is under active experimentation and is not yet guaranteed fit for any particular purpose.

References

• Homotopy Type Theory in Isabelle. ITP 2021. DOI: 10.4230/LIPIcs.ITP.2021.12
• An Implementation of Homotopy Type Theory in Isabelle/Pure. arXiv:1911.00399 [cs.LO]

Usage

Isabelle/HoTT is compatible with Isabelle2021. To use, add the Isabelle/HoTT folder path to .isabelle/Isabelle2021/ROOTS (on Mac/Linux/cygwin installations):

$ echo path/to/Isabelle/HoTT >> ~/.isabelle/Isabelle2021/ROOTS

To-do list

In no particular order.

• Dedicated type context data
• Definitional unfolding, better simplification in the typechecker
• Proper handling of universes
• Recursive function definitions
• Inductive type definitions
• Higher inductive type definitions

isabelle-hott's Issues

Rules are not grouped well for automation

The way the type rules and other derived rules are currently grouped is not optimal for automated proof methods.

At the moment the grouping is by type, e.g. type rules for the Equal type, Sum type etc. are bundled together, wellform rules are bundled together by type, etc.
I have a feeling it would be better to group the rules according to how they behave in proofs, e.g. formation rules should be grouped separately from the elimination/induction rules.

Automatic export of proof terms

Currently, we use schematic_goal to derive proof terms, then copy-paste the proof term in a new definition to be used in further proofs. It would be nice to automatically export derived proof terms, e.g.

schematic_goal my_lemma: "?prf: A"
proof
...
qed

should export the term derived by the schematic goal as my_lemma_prf.

Pure equality vs defined definitional equality

The theory thus far has been written to use the built-in Pure equality as the definitional equality, the idea initially being to take advantage of as much built-in functionality as possible.

However this creates may create differences between the implementation versus the formal type theory as presented in the book, e.g. the Martin-Löf type theory HoTT is based on does not have alpha-conversion, while the Pure equality does. [Edit: The situation is a little unclear. While the informal presentation in the HoTT book does mention alpha-conversion, the formalities in Appendix A2 do not really, and it's unclear how to use the existing judgment forms to express a change of bound variables.]

It would probably might be better to define a separate definitional equality on the object level for maximum compatibility with the theory in the book, though one would need to double check the theory.

Tactics looping on Isabelle2021

Certain tactics loop on Isabelle2021-RC3. Needs further investigation.

ascii-fy notation

Too much Isabelle/jEdit-only readable notation used in the current theory files, should probably change this.