Fabian Lukas Grubmüller: 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 Jrule makes the balance between benefits and downsides approximately equal