Jason (jcreed) wrote,

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.
Tags: math
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded