When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathrm{𝒮︀}\mathrm{ℯ︀}\mathrm{𝓉︀}$ , is replaced by the category $\mathrm{𝒽︀}\mathrm{𝒮︀}\mathrm{ℯ︀}\mathrm{𝓉︀}$ of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of $\mathrm{𝒮︀}\mathrm{ℯ︀}\mathrm{𝓉︀}$ hold for $\mathrm{𝒽︀}\mathrm{𝒮︀}\mathrm{ℯ︀}\mathrm{𝓉︀}$ ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that $\text{𝖮𝖻}\mathrm{𝒽︀}\mathrm{𝒮︀}\mathrm{ℯ︀}\mathrm{𝓉︀}$ is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example, when constructing internal models of type theory. In this work, we equip the type of iterative sets ${\text{𝖵}}^0$ , due to Gylterud ((2018). The Journal of Symbolic Logic 83 (3) 1132–1146) as a refinement of the pioneering work of Aczel ((1978). Logic Colloquium’77 , Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55–66.) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize ${\text{𝖵}}^0$ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of ${\text{𝖵}}^0$ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from ${\text{𝖵}}^0$ into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in $\text{𝙰𝚐𝚍𝚊}$ using the $\text{𝚊𝚐𝚍𝚊}$ - $\text{𝚞𝚗𝚒𝚖𝚊𝚝𝚑}$ library of univalent mathematics.

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky’s univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.