Internalizing representation independence with univalence. - Carlo Angiuli; Evan Cavallo; Anders Mörtberg; Max Zeuner (Proc. ACM Program. Lang., 2021)

A Univalent Formalization of Constructive Affine Schemes. - Max Zeuner; Anders Mörtberg (TYPES, 2022)

The Functor of Points Approach to Schemes in Cubical Agda. - Max Zeuner; Matthias Hutzler (ITP, 2024)

Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory. - Iosif Petrakis; Max Zeuner (Log. Methods Comput. Sci., 2024)

Univalent Constructive Algebraic Geometry: Foundations and Formalizations - Max Zeuner (2024)