My understanding of Pijul’s patch theory is that it is based on Mimram and Giusto’s paper “A Categorical Theory of Patches” where they model a merge as a pushout and describe a syntactic construction of the free (conservative) finite cocompletion of a category. The idea that a merge should be a pushout seems well-motivated to me, but their specific model of the category of patches seems wrong.
Their model of “increasing” patches seems fine, but their model of patches with deletion forms a (connected) groupoid: every object is equivalent because you can just delete all the lines of the file and then add the lines in the other version. This would mean that any file state could be a valid merge, including always producing the empty file. I have searched for mention of this problem and only found this comment on reddit which is probably where I first heard about this problem.
How is this problem addressed in pijul? It seems to me that the objects of the category should incorporate some amount of the “history” of the object that does monotonically increase, in order to make deleting and restoring not an isomorphism, but I haven’t worked out any details. This blog post describes “ghost lines” but not very formally. Is there something more formal in the pijul repo?