Quotient inductive types and QW types

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

• Shaun Steenkamp (University of Cambridge)
• Friday 28 May 2021, 11:00-12:00
• https://meet.google.com/jxy-edcv-wgx.

If you have a question about this talk, please contact Nathanael Arkor.

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 .

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

• Logic & Semantics for Dummies
• https://meet.google.com/jxy-edcv-wgx
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.