Figured out a cute little fact about the logic of proof irrelevance, I think: that the proof irrelevant modality is essentially two independent and otherwise "abstract" monads (in the sense that there are no primitive computations populating their types) in sequence. That is, make up monads M1 and M2. Then "proof-irrelevantly A" can be adequately translated (in a simply-typed system!) to M1 (M2 A). I had the idea this Friday last, and as of now I have a complete sketch of a proof, but it bears some writing down carefully to see if it's really right.