Evan Cavallo: Observational Type Theories
Time: Wed 2022-10-19 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Evan Cavallo (Stockholm University)
Abstract
I'll give a survey of Altenkirch, McBride, and Swierstra's observational type theory (OTT) and its descendants. In contrast to intensional Martin-Löf type theory, where equality types inductively generated by definitional equality, the OTT type of equalities in a type A is defined by recursion on the structure of A. The idea is that two elements are equal when they have the same behavior under appropriate observations: pairs are equal when their components are equal, functions are equal when they take equal values on all arguments. Moreover, the equality type is proof-irrelevant. I'll introduce the original OTT as well as Sterling, Angiuli, and Gratzer's re-imagination of OTT inspired by cubical type theory, called XTT, and recent work of Pujet and Tabareau.