-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2021.QuotientInductiveInductiveTypes
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.
-
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani. Containers: Constructing strictly positive types. 2005.
-
Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, Peter Morris. Indexed containers. 2009, 2015.
-
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.