Abstracts.2021.QuotientInductiveInductiveTypes

Quotient inductive-inductive types

by Szumi Xie

Abstract

In this talk, I will introduce quotient inductive-inductive types (QIITs), which are a generalization of inductive types. It allows types to index over each other while also mutually referring to each other, it also adds proof-irrelevant equality constructors. The syntax of type theory itself can be defined as a QIIT, I will show a fragment called the theory of signatures, which can be used to specify all QIITs, where the signature of a QIIT is the context in the theory of signatures.

References

• Ambrus Kaposi and Zongpu (Szumi) Xie. Quotient inductive-inductive types in the setoid model. 2021.