See QIIT (Project).
Follow-Up Actions
- Write a summary of the meeting
- Set up next supervision date
- Create reading list
Meeting Summary
- 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 choice.
- Compiled a reading list and outlined immediate research and development next steps.
Universal Quotient Inductive-Inductive Types
Reading List (“Before next meeting”)
- 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” Additional References:
- 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”
- Mortberg et al. 2020 “For Finitary Induction-Induction, Induction Is Enough”
- Kaposi 2016 PhD Thesis “Type Theory in a Type Theory with Quotient Inductive Types”
Key Definitions to Review
- Quotient Inductive-Inductive Types (QIIT)
- Infinitary QIIT
- Countable Choice
- Uncountable Choice
- Self-Hosting Type Theory
- Partiality (Type Theory)
- W Type
- M Type
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.