-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2021.QuotientInductiveInductiveTypes
Fabian edited this page Dec 9, 2021
·
5 revisions
by Szumi Xie
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.
- Gabe Dijkstra. Quotient inductive-inductive definitions. 2017.
- Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg. Quotient Inductive-Inductive Types. 2018.
- Ambrus Kaposi, András Kovács and Thorsten Altenkirch. Constructing quotient inductive-inductive types. 2019.
- András Kovács and Ambrus Kaposi. Large and Infinitary Quotient Inductive-Inductive Types. 2021.
- Ambrus Kaposi and Zongpu (Szumi) Xie. Quotient inductive-inductive types in the setoid model. 2021.