Constructing Infinitary Quotient-Inductive Types

Add to your list(s) Download to your calendar using vCal

• Andy Pitts (University of Cambridge)
• Friday 10 January 2020, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

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

Quotient-inductive types (QITs) intertwine the inductive construction of data and rules for identifying that data. They are the one-dimensional special case of higher inductive types from Homotopy Type Theory and have been popularised by Altenkirch and his co-authors.

At first sight it seems that in constructive type theories QITs are more expressive than the combination of ordinary inductive types with quotient types. This is because they permit infinitary constructs that appear to need the axiom of choice to be modelled using ordinary quotients. However, for a wide class of QITs, called QW-types, with some ingenuity choice can be avoided: these QITs can be expressed using the combination of inductive-inductive definitions, Hofmann-style quotient types, and Abel’s version of size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of QW-types.

The development has been formalised using the Agda theorem-prover and is joint work with Marcelo Fiore and Shaun Steenkamp.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.