Repository for Agda code associated with my master thesis (UiB 2021/22)

• hpt-formalization contains formalizations of Angiuli et al.'s homotopical patch theory in Cubical Agda including:
  • 4. An elementary patch theory
  • 5. A patch theory with laws (and in particular the "program and prove" approach of 5.3)
  • 6. A patch theory with richer contexts (without laws, an incomplete version with patch laws here)
• experiments contains various attempts at different formulations of version control systems as HITs
• trash-can contains more attempts, but ones I am even less happy with