BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Choice Principles in Observational Type Theory - Loïc Pujet (Univ
 ersity of Stockholm)
DTSTART:20240308T140000Z
DTEND:20240308T150000Z
UID:TALK212986@talks.cam.ac.uk
CONTACT:47138
DESCRIPTION:Observational Type Theory is an internal language for types eq
 uipped with a proof-irrelevant propositional equality. As such\, it native
 ly supports extensionality principles\, UIP\, and quotients of types by pr
 oof irrelevant relations (à la Lean).\n\nUnfortunately\, it is difficult 
 to use these quotients without any choice principles to extract informatio
 n from proof-irrelevant truncations. In this talk\, I will discuss the var
 ious choice principles one could hope to have in OTT\, and I will use idea
 s from Higher Observational Type Theory to sketch a version of OTT with un
 ique choice.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR