I have this notion that the proof irrelevance modality ought to be logically equivalent to the composition of two distinct monads — just enough to cause it to not be idempotent — but I can't prove one direction of the equivalence I expect to hold.
I have this notion that the proof irrelevance modality ought to be logically equivalent to the composition of two distinct monads — just enough to cause it to not be idempotent — but I can't prove one direction of the equivalence I expect to hold.
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
