Homotopy Type Theory in Isabelle
Abstract
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.
Keywords
Cite
@article{arxiv.2002.09282,
title = {Homotopy Type Theory in Isabelle},
author = {Joshua Chen},
journal= {arXiv preprint arXiv:2002.09282},
year = {2021}
}
Comments
Thoroughly revised version; accepted for publication at the 12th International Conference on Interactive Theorem Proving (ITP 2021). 8 pages, 1 figure