Frustrated by over a month of being too busy to work on Epigram 2, I’m hiding in Wales and hacking. As part of the next move towards observational equality, I’ve added a heterogeneous operator (a:A) <=> (b:B) which computes to a type packaging the appropriate premises from which (a:A) = (b:B) might be concluded. I’m not totally sure it’s wise to do so, but we’ll see. It’s certainly fun to play with. I guess I’ll write up some more formal details shortly.
When I recently tried to find out how I happened to write the same ap of the double negation Idiom twice by tracing identities with reflexity, I wondered how OTT’s λ⁼ constructor might get along with implicit argument abstraction.