The Category of Iterative Sets in Cubical Agda

Abstract

Iterative sets form a constructive Tarski-style universe V⁰ of h-sets. This universe is closed under common type-theoretic constructions and is itself an h-set. It arises naturally from the study of iterative multisets, where V⁰ is defined as a specific type-indexed W-type for which the indexing function is restricted to embeddings, effectively collapsing higher structure.

In previous work, Gratzer, Gylterud, Mörtberg, and Stenholm showed that V⁰ is a model of dependent type theory, in particular a Category with Families (CwF), that admits both Π- and Σ-structures. While their proofs were rather straightforward on paper, often reducing to reflexivity, their formalization in standard Agda (using agda-unimath) faced significant obstacles. For the formalization of Π- and Σ-structures, they faced problems due to complex path algebra involving multiple layers of transport and function extensionality, leading them to abandon the formalization of the Σ-structure.

In this thesis, we explore whether a formalization in Cubical Agda, an extension of Agda for cubical type theory, is easier to accomplish. We implement the general properties of iterative sets, as well as CwF and Σ-structures. For the latter we use three distinct strategies: a naive translation of the prior work, a more cubical approach replacing equalities containing transport with heterogeneous path types, and a strategy that eliminates transport in favor of ad-hoc functions that can be later instantiated by the identity function. We find that while the cubical metatheory simplifies reasoning about extensionality, it also introduces new challenges. One of the main issues is the lack of a definitional J-rule in Cubical Agda, which means that certain terms do not compute definitionally, requiring manual handling of transport structures. Ultimately, we are also unable to finish the proof of the naturality condition for Σ-structures due to the inherent complexity of the goal types. However, our approach substantially simplifies the remaining proof goals, which makes us hopeful that the proof will be able to be completed in future work. We conclude that while Cubical Agda improves clarity in specific areas, we concede that the trade-off regarding the definitional behaviour of the J-rule makes the balance between benefits and downsides approximately equal.

Cite

Hayagriva YAML

cubical-iterative-sets:
  type: Thesis
  title: The Category of Iterative Sets in Cubical Agda
  author: Grubmüller, Fabian Lukas
  date: 2026-01-14
  organization: Stockholm University
  url: "https://grubmueller.dev/publications/2026-mt-iterative-sets/"
  note: Master thesis

BibTeX

@mastersthesis{cubical-iterative-sets,
    title = {The Category of Iterative Sets in Cubical Agda},
    author = {Grubm\"{u}ller, Fabian Lukas},
    year = {2026},
    school = {Stockholm University},
    type = {Master thesis},
    note = {\url{https://grubmueller.dev/publications/2026-mt-iterative-sets/}},
}

Notes

Type: Master Thesis
Supervisor: Anders Mörtberg
Programme: Mathematics M.Sc.
University: Stockholm University (joint with KTH Royal Institute of Technology)