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)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

  • (no subject)

    Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…

  • 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 

  • 3 comments