A Cubical Implementation of Homotopical Patch Theory

Abstract

We consider theoretical models of version control systems based on Homotopy Type Theory (HoTT). The main contribution is an implementation of Angiuli et al.’s Homotopical Patch Theory in Cubical Agda. Additionally the first chapter contains an approachable introduction to HoTT and Cubical Agda aimed at an audience of interested computer science students covering dependent Martin-Löf-style type theory, propositions as types, univalent foundations, higher inductive types and CCHM cubical type theory. Finally, we discuss some other approaches to a theory of version control systems in Darcs’ “algebra of patches” and an unsuccessful attempt to model repositories in type theory as coequalizers.