University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Choice Principles in Observational Type Theory

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Choice Principles in Observational Type Theory

Download to your calendar using vCal

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

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:

Note that ex-directory lists are not shown.

Other lists

Webinar (via Zoom online) ID: 87457263100 Passcode: 708172 Room W4.05, Cambridge Judge Business School, Trumpington Street Old Combination Room, Trinity College, Cambridge. CB2 1TQ

Other talks

Unveiling the curtain with ukubuyisa or go lata: complicated roles of museums and nation states in the cultural repatriation discourse and practice in southern Africa TBC Sera Markoff Inaugural Lecture for the Plumian Professorship in Astronomy and Experimental Philosophy - 'Staring into the heart of darkness: from theory to the direct imaging of black holes' Title to be confirmed The Inaccessible Game Topology of the Ritz energy landscape
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity