BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Constructing Infinitary Quotient-Inductive Types -
Andy Pitts (University of Cambridge)
DTSTART:20200110T110000Z
DTEND:20200110T120000Z
UID:TALK4081AT
URL:/talk/index/4081
DESCRIPTION:Quotient-inductive types (QITs) intertwine the ind
uctive construction\nof data and rules for identif
ying that data. They are the\none-dimensional spec
ial case of higher inductive types from Homotopy\n
Type Theory and have been popularised by Altenkirc
h and his\nco-authors.\n\nAt first sight it seems
that in constructive type theories QITs are\nmore
expressive than the combination of ordinary induct
ive types with\nquotient types. This is because th
ey permit infinitary constructs that\nappear to ne
ed the axiom of choice to be modelled using ordina
ry\nquotients. However\, for a wide class of QITs\
, called QW-types\, with\nsome ingenuity choice ca
n be avoided: these QITs can be expressed\nusing t
he combination of inductive-inductive definitions\
,\nHofmann-style quotient types\, and Abel's versi
on of size types. The\nlatter\, which provide a co
nvenient constructive abstraction of what\nclassic
ally would be accomplished with transfinite ordina
ls\, are used\nto prove termination of the recursi
ve definitions of the elimination\nand computation
properties of QW-types.\n\nThe development has be
en formalised using the Agda theorem-prover and\ni
s joint work with Marcelo Fiore and Shaun Steenkam
p.
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Dan Ghica
END:VEVENT
END:VCALENDAR