QIIT (Project)

Abstract

Type theory is a constructive approach of logic, meaning all existence claims ($\exists x\text{ s.t.}P(x)$) may only be satisfied by an explicit witness: $(x,p)$ where $p$ is a proof of $P(x)$. This differs from classical logic, in which statements such as $P\text{ or not }P$ are assumed a priori. Type theories play a foundational role in the formalisation of logical proofs — the effort to verify the correctness of mathematical proofs using computer-aided verification. This is useful in verifying mathematical theorems, as well as proving safety properties of software systems. The research goal is the formalization of a type theory that can represent the syntax and semantics of other type theories (and itself, i.e. self-hosting). Significant progress has been made toward in this goal past 10 years, through the use of ‘quotient inductive-inductive types’, which are a combination of the following:

• quotient inductive types: types made from one of a set of certain constructors which allow for equations of elements.
• inductive-inductive types: a way of defining inductive types simultaneously, e.g. a types A and B can be constructed even when B is indexed by A and A may refer to constructors involving B. The aim is to help in developing a type theory that admits universal and possibly infinitary QIITs, ensuring consistency, self-hosting, and non-reliance on non-constructive proofs.

Meetings

PhD meeting 20251002

• Initial supervision meeting with Prof. Thorsten Altenkirch.
• Discussion focused on familiarization with quotient inductive-inductive types (QIITs), especially the concept of universal QIIT.
• The research goal is to work toward a type theory that admits universal and possibly infinitary QIITs, ensuring consistency, self-hosting, and non-reliance on classical principles like LEM or uncountable Axiom of Choice.
• Compiled a reading list and outlined immediate research and development next steps.

PHD Meeting 20251009

Key Research Questions

RG1

How to define QW-types in a computable and practical way? We are looking for a concise version of a QW type which captures all QITs and QIITs. Going further we may want the same for higher inductive types (HW). This is a motivation not clear to what degree we can actually achieve this. What are QIITs reducible to? (See kaposi2019-constructing-qiit, fiore2022-quotient-inductive, fiore2020-infinitary-qiit.)

RG2 - solved see Thorsten slides 2020

Can inductive-inductive types be defined with only inductive types?

RG3

How can QIITs be used to define type theories. See kaposi2016-type-theory-in-type-theory

RG5

How to define the Capretta partiality monad (capretta2005-partiality), and what principles (e.g., countable choice) are needed?

RG6

Relationship between partial computation, axiom of choice, and LEM; partiality as an effect in type theory.

Reading List

• Altenkirch et al. 2016 “Quotient Inductive-Inductive Types”
• Kaposi et al. 2019 “Constructing Quotient Inductive-Inductive Types”
• Damato 2025 “Formalising Inductive and Coinductive Containers”
• Fiore et al. 2022 “Quotients, Inductive Types, and Quotient Inductive Types”
• Kovacs & Kaposi 2020 “Large and Infinitary Quotient Inductive-Inductive Types”
• Altenkirch et al. 2016 “Partiality, Revisited”
• Altenkirch & Kaposi 2016 “Type Theory in Type Theory using Quotient Inductive Types”
• Altenkirch 2024 “Quotient Inductive Types as Categorified Containers”
• Kaposi & Kovacs 2017 “Codes for Quotient Inductive Inductive Types?”
• Fiore et al. 2020 “Constructing Infinitary Quotient-Inductive Types”
• Dijkstra 2017 PhD Thesis “Quotient Inductive-Inductive Definitions”
• Altenkirch & Kaposi 2021 “A Container Model of Type Theory”
• Kaposi et al. 2019 “For Finitary Induction-Induction, Induction Is Enough”
• Kaposi 2016 PhD Thesis “Type Theory in a Type Theory with Quotient Inductive Types”

Review

fiore2022-quotient-inductive & pitts2021-inflationary-iteration: MLTT+UIP+ext+Prop+A!C+WISC proves existence and initiality of QWI types.

fiore2020-infinitary-qiit:
MLTT+UIP+quotients+sized types proves existence and initiality of QW types.

kaposi2019-constructing-qiit:
MLTT+UIP+one signature-QIIT proves existence and initiality of all finitary QIITs.

kovacs2020-infinitary-qiit:
MLTT+UIP+structured CwF proves existence and initiality of infinitary QIITs.

altenkirch2016-qiit: MLTT+UIP proves (initiality ↔ induction) for finitary QIIT signatures.

dijkstra2017-thesis-qiit: MLTT+UIP+quotients proves (initiality ↔ induction) and constructs many QIITs by colimits.

altenkirch2016-partiality: HoTT+UIP proves existence and initiality of the partiality monad as a QIIT.

altenkirch2016-type-theory-qit:
MLTT+UIP+QIT primitives proves existence and initiality of an intrinsically typed syntax QIT.

collem2025-initial-domain-qiit: Cubical+UIP+QIIT primitives proves existence and initiality of domain-theoretic QIITs.

Kovács (2023): MLTT+UIP proves existence and initiality principles for finitary, infinitary, and higher QIIT signature theories.

Glossary

MLTT: intensional Martin-Löf type theory.
ext: extensional definitional equality for functions and propositions.
UIP: uniqueness of identity proofs.
Prop: impredicative universe of proof-irrelevant propositions.
unique choice: extraction of witnesses from unique existence.
WISC: weakly initial set of covers.
quotients: set-level quotient types.
sized types: size-indexed recursion for termination.
QIT/QIIT/QIID: quotient-inductive types, possibly inductive-inductive.
CwF: category with families.

Key Definitions to Review

• quotient inductive-inductive types (QIIT)
• quotient inductive-inductive types > Finitary
• Countable Choice
• Uncountable Choice
• Self-Hosting Type Theory
• Partiality (Type Theory)
• W Type
• M Type
• Container

Progress Update

• MSc dissertation submitted.
• Continued development of virtual sets in Agda; working on monoidal categories and defining naturality of associator.

Actions and Next Steps

• Continue Agda work on virtual sets and construct naturality squares via transport.
• Read key papers, make detailed notes, and be prepared to discuss current challenges and open questions in QIITs during the next supervision.