New ICFP functional pearl on subtracting bijections

Kenny Foner and I have a paper accepted to ICFP on subtracting bijections. Here’s the basic problem: suppose you have a bijection \(h\) between two sum types, \(h : A + B \leftrightarrow A' +B'\), and another bijection \(g : B \leftrightarrow B'\). Of course \(A\) and \(A'\) must have the same size, but can you construct an actual bijection \(f\) between \(A\) and \(A'\)?

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.