2014/08/19 by Carlo Angiuli, Edward Morehouse, Daniel R. Licata +1 · 1 voice · 1 citation
Computer Science · #Advanced Database Systems and Queries #Logic, programming, and type systems #Security and Verification in Computing
paper · doi:10.1145/2628136.2628158
openalex publication_date 2014/08/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
Homotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type becomes proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches - syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.