# 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.