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.