1. "not understanding the relevance of this paper to distributed version control"; 18. "what the point is.": On page 11: Our contribution [..] is to present patch theory in a categorical setting that is also a programming formalism, so it directly leads to an implementation.
2.: Patches are (homotopically) equivalent to paths and form inductive groupoids. (pg 11) "In homotopy type theory the path space of every type is symmetric, and to fit patch theories into this symmetric setting, we either considered a language where all patches were naturally total bijections on any repository (Section 4 and 5), or used types to restrict patches to repositories where they are bijections" Inverses of patches arise due to these considerations. The use of the term distributed seems to be used in the sense of dependence that arises with pseudocommutation (pcom).
3. It might be inferred that apd = Action on Paths for Dependent function (f) Action on inductive groupoids. (https://ncatlab.org/nlab/show/fiber+sequence#ActionGroupoid) So, a fiber sequence? Not sure where it is stated that PathOver does not depend on f (along with p and B)?
7. section 6 uses histories that are a quotient higher inductive type to equate sequences of patches, which result in the same changes to a file.
11. "Pseudocommutation gives us a merge operation that is well-defined, symmetric [..], and reunites the two branches of a span, but this is not enough to guarantee that we get the merges that we might expect" ..
12. "the correctness of pseudocommutation follows from the induction principles for paths that are proved for each type from the basic induction principles for the higher inductive types—roughly analogously to how, for the natural numbers, course-of-values induction is derived from mathematical induction. Moreover, proving these induction principles is sometimes a significant mathematical theorem. In homotopy theory, it is called calculating the homotopy groups of a space, and even for spaces as simple as the spheres some homotopy groups are unknown."
15.; 16. see section 6 for a patch language with add and remove, not just swap. Unfortunately, the authors were unable to provide a proof of the correctness of the proposed pcom (p,q) definition for it. If it is correct, it would be a more general patch language than the merges as pushout with ojo pseudo-edge proposal along with its assumptions / restrictions on deletions that computes patch application by having [multiple] Tarjan (2-SAT) run(s). Even so, not sure how efficiently the "length-2 suffix" pcom would work out. Reminder that dependency resolution is NP complete.
17. "In homotopy type theory the path space of every type is symmetric"
18. If merges could be assumed to be push outs or proved to be that would remove the ambiguity arising from pcom -> imply its correctness. pcom is defined for each patch language. Section 6.4 gives an outline on how to use patch laws to prove the correctness of the assumed pcom definition. The references also provide further details [18], [19], etc. The "category" paper ref treats merge as a pushout not as pcom based. pcom may be seen as a generalization of merges as pushouts. For another perspective on what is the same mathematical structure regarding Darcs see the Jacobson [15] reference that interprets patches as inverse semigroups, which are essentially partial bijections. Additionally, the Ehresmann-Schein-Nambooripad theorem states that inverse semigroups are equivalent to inductive groupoids.
NB I am not an author of any of the papers.