Abstract

Joint work with A. M. Pitts and M. P. Fiore.

Quotient inductive types (QITs) are the notion obtained by considering higher inductive types (HITs) in a type theory with uniqueness of identity proofs (a.k.a axiom K).

QITs generalise inductive types by allowing equations, allowing, for example,

Circle : 𝓤 base : Circle loop : base = base

where the loop constructor “lands” in the Martin-Löf identity type on Circle. Other examples include un-ordered trees, or finite multisets (represented as unordered lists).

In this talk I will give an introduction to quotient inductive types (QITs), and then define QW-types, which we introduce 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 construction of QW types. Specifically, by constructing QW-types, we show that QITs exist in MLTT with Universes, UIP , and WISC .