I've been staring at this for a day, and it all just hit me like brick and seems obvious now!

Thanks John & commenters!

The construction of P \/ Q reminds me very much of how free categories, monoids, monads etc are constructed (ie induction), might it be regarded as some kind of free coproduct or something?

Also, it reminds me of the asymmetry between the straightforward product of monoids vs the complicated coproduct of monoids, is this related somehow to partition joins?