Loïc Pujet: Indexed inductive types in Observational Type Theory
Time: Wed 2023-06-21 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Loïc Pujet, Stockholm University
Abstract
Observational Type Theory (OTT) was designed by Altenkirch, McBride and Swierstra to extend MLTT with function extensionality and the uniqueness of identity proofs, while preserving most of its computational properties. It can be thought of as a type theory for setoids with a proof-irrelevant equality, just like Cubical Type Theory is a type theory for fibrant cubical sets.
The aim of this talk is to present joint work with Nicolas Tabareau on implementing OTT in the Coq proof assistant. In particular, I will explain how we handle the full scheme of indexed inductive types of Coq, without breaking compatibility with the existing Coq syntax.