(based on joint work with Conor McBride, Nicolas Oury and Wouter Swierstra)
Martin-Loef Type Theory comes in two variants: Extensional Type Theory which supports extensional mathematical reasoning but is undecidable and Intensional Type Theory which is decidable but forces us to reason intensionally, loosing common means of abstraction. In this talk I will introduce an alternative, which we call "Observational Type Theory" with the goal of combining exensional reasoning with decidability.