BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Quotient inductive types and QW types - Shaun Steenkamp (Universit
 y of Cambridge)
DTSTART:20210528T100000Z
DTEND:20210528T110000Z
UID:TALK160786@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:Joint work with A. M. Pitts and M. P. Fiore.\n\nQuotient induc
 tive types (QITs) are the notion obtained by considering higher inductive 
 types (HITs) in a type theory with uniqueness of identity proofs (a.k.a ax
 iom K).\n\nQITs generalise inductive types by allowing equations\, allowin
 g\, for example\,\n\nCircle : 𝓤\nbase : Circle\nloop : base = base\n\nw
 here the loop constructor “lands” in the Martin-Löf identity type on 
 Circle. Other examples include un-ordered trees\, or finite multisets (rep
 resented as unordered lists).\n\nIn this talk I will give an introduction 
 to quotient inductive types (QITs)\, and then define QW-types\, which we i
 ntroduce for the role of universal QIT. That is\, QW-types are to QITs as 
 W-types are to inductive types. I will then give an outline of our constru
 ction of QW types. Specifically\, by constructing QW-types\, we show that 
 QITs exist in MLTT with Universes\, UIP\, and WISC.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR