University of Cambridge > Talks.cam > Logic & Semantics for Dummies > Quotient inductive types and QW types: part II

Quotient inductive types and QW types: part II

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity