Friday 15 December 2023, 13:00, room 1Z71 (or online): Countable choice in Observational Type Theory, Loïc Pujet (University of Stockholm).

Observational Type Theory is an internal language for types equipped with a proof-irrelevant propositional equality. As such, it natively supports extensionality principles, UIP, and quotients of types by proof-irrelevant relations (à la Lean).Unfortunately, it is difficult to use these quotients without any choice principles to extract information from proof-irrelevant truncations.In this talk, I will use ideas from Higher Observational Type Theory to sketch a version of OTT that supports countable choice for Delta00 predicates.