BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:Quotient inductive types and QW types: part II - S
haun Steenkamp (University of Cambridge)
DTSTART;TZID=Europe/London:20210604T110000
DTEND;TZID=Europe/London:20210604T120000
UID:TALK160927AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/160927
DESCRIPTION:Joint work with A. M. Pitts and M. P. Fiore.\n\nQu
otient inductive types (QITs) are the notion obtai
ned by considering higher inductive types (HITs) i
n a type theory with uniqueness of identity proofs
(a.k.a axiom K).\n\nQITs generalise inductive typ
es by allowing equations\, allowing\, for example\
,\n\nCircle : đť“¤\nbase : Circle\nloop : base = base
\n\nwhere the loop constructor â€ślandsâ€ť in the Mart
in-LĂ¶f identity type on Circle. Other examples inc
lude un-ordered trees\, or finite multisets (repre
sented as unordered lists).\n\nIn this talk I will
give an introduction to quotient inductive types
(QITs)\, and then define QW-types\, which we intro
duce for the role of universal QIT. That is\, QW-t
ypes are to QITs as W-types are to inductive types
. I will then give an outline of our construction
of QW types. Specifically\, by constructing QW-typ
es\, we show that QITs exist in MLTT with Universe
s\, UIP\, and WISC.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR