The Category of Iterative Sets in Cubical Agda

Iterative sets form a constructive Tarski-style universe V⁰ of h-sets that is itself an h-set. It arises naturally from the study of iterative multisets, where V⁰ is defined as a particular W-type for which the indexing function is restricted to embeddings. In previous work, Gratzer, Gylterud, Mörtberg, and Stenholm showed that V⁰ can be equipped with the structure of a Category with Families, that admits both Π- and Σ-structures. While their proofs were rather straightforward on paper, their Unimath Agda formalization faced significant obstacles, particularly for the Σ-structures.

In my master’s thesis, I explored whether a formalization of this using Cubical Agda would be easier, which ultimately turned out not to be the case. In this talk, I will present the results and challenges of this effort as well as the continuing work together with Anders Mörtberg and Peter Lumsdaine.