Observational equality, now!

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 which is substitutive , allowing us to reason by replacing equal for equal in propositions; which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality -- functions are equal if they take equal inputs to equal outputs; which retains strong normalisation, decidable typechecking and canonicity --the property that closed normal forms inhabiting datatypes have canonical constructors; which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees ; which is presented syntactically --you can implement it directly, and we are doing so this approach stands at the core of Epigram 2; which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21]. .