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 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

• http://real.mtak.hu/130779/1/TYPES21%20-%20Quotient%20inductive-inductive%20types%20in%20the%20setoid%20model%20%28Kaposi%20and%20Xie%29.pdf