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

3 hours 26 min ago

7 hours 5 min ago

13 hours 41 min ago

15 hours 9 min ago

19 hours 19 min ago

19 hours 36 min ago

21 hours 23 min ago

22 hours 8 min ago

1 day 1 hour ago

1 day 1 hour ago