Kenny Foner and I have a paper accepted to ICFP on subtracting bijections. Here’s the basic problem: suppose you have a bijection 
This problem and its solution has been well-studied in the context of combinatorics; we were wondering what additional insight could be gained from a higher-level functional approach. You can get a preprint here.
blog :: Brent -> [String] 
I’m a bit confused about the definition of compatibility (section 5): doesn’t this define usual function equality? I would expect compatibility to be something like “If f a = Just b1 and g a = Just b2, then b1 = b2”.
You’re absolutely right, thanks for the correction! Not sure how I missed that. =) Fortunately it is not too late, we haven’t turned in the camera-ready version yet.
I only skimmed, but this proof structure feels a lot like schroder-bernstein: https://en.wikipedia.org/wiki/Schr%C3%B6der%E2%80%93Bernstein_theorem
Are you aware of any connections in this direction?
Wonderful graphics and exposition :)
Yes, it does have a similar feel to it! I haven’t thought too much about the exact connection (if there is one).
In section 4, are you mixing A’ with B? I am thinking of the sentences about “recycling” elements which land in B. From the figure, it seems to me that it’s the elements that land in A’ that get recycled back to their original positions in A, while elements that land in B’ are carried on through the bijection until they land in A’.
Otherwise a very readable paper!