University of Birmingham > Talks@bham > Theoretical computer science seminar > Constructing Infinitary Quotient-Inductive Types

Constructing Infinitary Quotient-Inductive Types

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.