This licentiate thesis consists of two papers on formalization projects using Cubical Agda, a rather new extension of the Agda proof assistant with constructive support for univalence and higher inductive types. The common denominator of the two papers is that they are concerned with structures on types that are sets in the sense of Homotopy Type Theory or Univalent Foundations (HoTT/UF). Univalence gives rise to the so-called structure identity principle (SIP) that plays a prominent role in both papers. This thesis can thus be seen as an investigation into working with “set-level structures” in HoTT/UF.

The first paper explains the basics of the SIP implemented in Cubical Agda’s library and is concerned with its application in computer science. In particular, the paper shows how the SIP, when applied to common data structures, can guarantee representation independence internally for certain implementations. These implementations have to be isomorphic in the sense of the SIP. The paper also generalizes the SIP to a relational version that can account for wider classes of implementations.

The second paper is concerned with the formalization of affine schemes, a central notion of algebraic geometry. It combines a constructive and point-free approach to schemes with univalence. Schemes have been formalized in several proof assistants by now, but standard textbook presentations often gloss over certain details that in a formalization become very cumbersome to prove. The main result of this paper is that with the help of univalence, or rather the SIP for commutative rings and algebras over a commutative ring, we can directly formalize affine schemes in a way that more closely resembles the standard textbook approach.

This thesis contains four papers concerned with Homotopy Type Theory and Univalent Foundations (HoTT/UF) and its use as a foundation to study constructive approaches to the theory of schemes, a fundamental notion in algebraic geometry. The main results of this project are presented in the first paper. The other three papers present formalizations of several of these results in Cubical Agda, an extension of the Agda proof assistant with constructive support for univalent foundations. The individual contributions of the papers are as follows.

The first paper, "Univalent Foundations of Constructive Algebraic Geometry", investigates two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes) in HoTT/UF, namely qcqs-schemes as locally ringed lattices and as functors from rings to sets. The main result is a constructive and univalent proof that the two definitions coincide, giving an equivalence between the respective categories of qcqs-schemes.

The second paper, "Internalizing Representation Independence with Univalence", discusses an implementation of the so-called structure identity principle (SIP), an important consequence of univalence employed in the other papers, in Cubical Agda and studies its applications in computer science. It is shown that the SIP guarantees representation independence internally for isomorphic implementations of common data structures. The SIP is then generalized to a relational version that can account for wider classes of implementations.

The third paper, "A Univalent Formalization of Constructive Affine Schemes", presents a formalization of affine schemes as ringed lattices in Cubical Agda. Standard textbook presentations of the structure sheaf of an affine scheme often gloss over certain details that turn out to be a serious obstacle when formalizing this construction. The main result of this paper is that with the help of univalence, or rather the SIP for rings and algebras, one can formalize affine schemes in a way that resembles the standard textbook approach more closely than previous formalizations of (affine) schemes in other proof assistants.

The fourth paper, "The Functor of Points Approach to Schemes in Cubical Agda", presents a formalization of qcqs-schemes in Cubical Agda, using Grothendieck's functor of points approach. This is the first formalization following this alternative approach and the first constructive formalization that manages to get beyond affine schemes. The main result is a streamlined definition of functorial qcqs-schemes allowing for a fully formal and constructive proof that compact open subfunctors of affine schemes are qcqs-schemes.