[darcs-devel] clean merge and pushouts in a groupoid

[Ben Franksen]

I am struggling with the following quite elementary problem in applied
category theory.

In order to give a full specification of the clean merge of two patch
sequences, I want to express that the result of the clean merge is
"minimal"; in particular, it should not contain any common patches.

Inspired by the idea of the paper that laid the groundwork for Pijul, I
thought this could be formulated abstractly by requiring that
cleanMerge, if it succeeds, is a pushout: if cleanMerge (p:\/:q) = Just
(q':/\:p'), where (p:>q'), (q:>p') :: p wX wY, then for any other pair
(q'':/\:p'') with (p:>q''), (q:>p'') :: p wX wZ, there is a unique r ::
p wY wZ such that

  p'' = p';r and q'' = q';r

i.e. the following diagram commutes:

        Z
       /|\
      / | \
     /  r  \
    |   |   |
   q''  |   p''
    |   Y   |
    |  / \  |
    | q'  p'|
    |/     \|
    o       o
     \     /
     p\   /q
       \ /
        X

The underlying category here is that of patch sequences, where we
identify all sequences that differ only by re-ordering patches and
insertion or removal of inverse pairs.

Now, this is not only a category, it is a groupoid, i.e. we can invert
any patch or patch sequence. And it seems to me that this means the
above requirement is vacuous: we can rename p' <-> p'', q' <-> q''  and
Y <-> Z, and it would still be commuting if we replace r <-> r^. And
that means /any/ pair with matching types is a pushout and the
requirement of clean merge being a pushout is useless. Indeed the whole
concept of pushout (or pullback) doesn't seem to make much sense in a
groupoid.

I am quite confused about this and would appreciate any kind of comment.