Jason (jcreed) wrote,
Jason
jcreed
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
Subscribe

  • (no subject)

    Still watching "Hell on Wheels". The characters motivations frequently make no sense at all, but at least they killed off the by-far most annoying…

  • (no subject)

    Watched some more "Hell on Wheels". Second season got dark fast.

  • (no subject)

    Tried watching ep 1 of "Hell on Wheels", which my dad recommended. It has a vaguely Deadwood feel, although the dialogue doesn't obviously sparkle…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 3 comments