Definition: A category X is said to be an inverse category whenever, for each arrow f : A -> B in X, there exists a unique f^ : B -> A in X such that ff^f = f and f^ff^ = f^.
(I write composition as juxtaposition without an operator.) Given a universe of extended invertible patches, define a category as follows: * Objects are the extended contexts. * Arrows are (finite) sequences of extended patches, with the identifications pp^p = p and p^pp^ = p^ and pq=q'p' whenever commute(pq)=q'p' (which I also write as pq<->q'p') * Composition is concatenation. * Identities are empty sequences (denoted id_X : X -> X). In other words, we start with the free inverse category on the graph of extended patches and factor that by the equivalence relation that identifies sequences that differ only up to commutation. This is also an inverse category because commutation respects inversion i.e. pq<->q'p' <=> q^p^<->q'^p'^, which is a consequence of the square-commute law. Some remarks: * I think in your theory you need to show that the squere-commute law holds for extended patches (assuming it does for primitive patches). * This construction works only if extended patches do have inverses i.e. not for Darcs. In Darcs we give up invertibility when we extend primitive patches, and instead define merging as a new "primitive" (sorry for overloading the term) operation. In your definition of extended patches invertibility falls out quite naturally, and indeed is required because you define merging in terms of inversion as in the primitive theory. So our arrows are equivalence classes of extended patch sequences. The construction is such that given a sequence P=...pp^p... we can reduce that to an equivalent smaller P'=...p... and I think it should be possible to show that all members of a class that are minimal (with respect to the length of the sequence) have the property that any patch they contain occurs at most once. (Formally: if names(P) is the set of names of patches occurring in P, then |names(P)|=length(P).) It is assumed that the primitive patch graph has a distinguished node (context) O that denotes an empty state with no files or directories. Since primitive contexts are embedded in extended contexts, we could then define a repository as an arrow in the inverse category of extended patch sequences that starts at O. Cheers Ben _______________________________________________ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users