Cover Image

A Univalent Formalization of Constructive Affine Schemes

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zeuner, Max, Mörtberg, Anders
Format:	Preprint
Published:	2022
Subjects:	Logic
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Internalizing Representation Independence with Univalence
by: Angiuli, Carlo, et al.
Published: (2020)

Univalent Foundations of Constructive Algebraic Geometry
by: Zeuner, Max
Published: (2024)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

The Functor of Points Approach to Schemes in Cubical Agda
by: Zeuner, Max, et al.
Published: (2024)

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
by: Ljungström, Axel, et al.
Published: (2023)

Computational Synthetic Cohomology Theory in Homotopy Type Theory
by: Ljungström, Axel, et al.
Published: (2024)

The Formal Theory of Monads, Univalently
by: van der Weide, Niels
Published: (2022)

Automating Boundary Filling in Cubical Type Theories
by: Doré, Maximilian, et al.
Published: (2024)

Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
by: Petrakis, Iosif, et al.
Published: (2022)

On Small Types in Univalent Foundations
by: de Jong, Tom, et al.
Published: (2021)

Univalence without function extensionality
by: Cavallo, Evan, et al.
Published: (2026)

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
by: Ambridge, Todd Waugh
Published: (2024)

(Pointed) Univalence in Universe Category Models of Type Theory
by: Kapulkin, Chris, et al.
Published: (2025)

Univalence and Ontic Structuralism
by: Chen, Lu
Published: (2024)

Derivatives for Containers in Univalent Foundations
by: Joram, Philipp, et al.
Published: (2025)

Constructive and Predicative Locale Theory in Univalent Foundations
by: Tosun, Ayberk
Published: (2026)

Univalent Double Categories
by: van der Weide, Niels, et al.
Published: (2023)

The Patch Topology in Univalent Foundations
by: Arrieta, Igor, et al.
Published: (2024)

Univalent Enriched Categories and the Enriched Rezk Completion
by: van der Weide, Niels
Published: (2024)

Epimorphisms and Acyclic Types in Univalent Foundations
by: Buchholtz, Ulrik, et al.
Published: (2024)

Trocq: Proof Transfer for Free, With or Without Univalence
by: Cohen, Cyril, et al.
Published: (2023)

A Graded Modal Dependent Type Theory with Erasure, Formalized
by: Abel, Andreas, et al.
Published: (2026)

Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda
by: Wißmann, Thorsten, et al.
Published: (2024)

Scott's Representation Theorem and the Univalent Karoubi Envelope
by: van der Leer, Arnoud, et al.
Published: (2025)

Univalent Material Set Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2023)

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
by: Bryce, Aaron, et al.
Published: (2026)

Constructive Ordinal Exponentiation
by: de Jong, Tom, et al.
Published: (2025)

Constructive Quantum Logics
by: Aguilera, Juan P., et al.
Published: (2025)

Three-Dimensional Affine Spatial Logics
by: Trybus, Adam
Published: (2026)

Meta-Modelling in Formal Concept Analysis
by: Wang, Yingjian
Published: (2024)

A Logic of Stability: Formalizing Similarity in Counterfactual Reasoning
by: Esteves, Marta
Published: (2025)

The Complexity of the Constructive Master Modality
by: Santiago-Fernández, Sofía, et al.
Published: (2026)

Affine Disjunctive Invariant Generation with Farkas' Lemma
by: Ke, Jingyu, et al.
Published: (2023)

A Formal Framework for Robot Construction Problems: A Hybrid Planning Approach
by: Ahmad, Faseeh, et al.
Published: (2019)

Formalizing two-level type theory with cofibrant exo-nat
by: Uskuplu, Elif
Published: (2023)

Formalization of the Filter Extension Principle (FEP) in Coq
by: Dou, Guowei, et al.
Published: (2024)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

Decidability and Complexity of Decision Problems for Affine Continuous VASS
by: Balasubramanian, A. R.
Published: (2024)

Constructive higher sheaf models with applications to synthetic mathematics
by: Coquand, Thierry, et al.
Published: (2026)

Affine Hulls and Simplices: a Constructive Analysis
by: Bridges, Douglas S.
Published: (2025)