A univalent formalization of constructive affine schemes

DOI10.4230/LIPICS.TYPES.2022.14MaRDI QIDQ6643044zbMATH OpenFDO

Authors Max Zeuner, Anders Mörtberg

Publication date 26 November 2024

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2022.14

zbMATH Keywords

affine schemesconstructive mathematicscubical agdahomotopy type theory and univalent foundations

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited in

(2)

• The functor of points approach to schemes in cubical Agda
• Grothendieck's use of equality

This page was built for publication: A univalent formalization of constructive affine schemes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6643044)