In Observational Equality, Now! Thorsten Altenkirch, Conor McBride, and Wouter Swierstra have

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]. Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Al- tenkirchâ€™s construction of a setoid-model for a system with canon- icity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirchâ€™s construction by adopting McBrideâ€™s heterogeneous ap- proach to equality.

## Recent comments

10 hours 10 min ago

11 hours 19 min ago

11 hours 19 min ago

11 hours 27 min ago

13 hours 36 min ago

21 hours 41 min ago

22 hours 50 min ago

23 hours 21 min ago

23 hours 28 min ago

23 hours 50 min ago