Formalizing Univalent Set-Level Structures in Cubical Agda

Sammanfattning: 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.