Choice Principles in Observational Type Theory

Add to your list(s) Download to your calendar using vCal

• Loïc Pujet (University of Stockholm)
• Friday 08 March 2024, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact nk480.

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 discuss the various choice principles one could hope to have in OTT , and I will use ideas from Higher Observational Type Theory to sketch a version of OTT with unique choice.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.