- 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