Observational equality, now!
Thorsten Altenkirch, Conor Thomas McBride, Wouter Swierstra · 2007
This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type