19 citations · 60 across the 11 of their papers we have counts for
13 papers
A Bézout domain that is not an elementary divisor domain
Christian Hägg, Anders Mörtberg
We settle in the negative the longstanding question whether every Bézout domain is an elementary divisor domain by constructing a Bézout domain over which an explicit m…
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
Daniel Gratzer, Håkon Gylterud, Anders Mörtberg +1
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types…
Automating Boundary Filling in Cubical Type Theories
Maximilian Doré, Evan Cavallo, Anders Mörtberg
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to rea…
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Axel Ljungström, Anders Mörtberg
This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation. The objectives of this paper are (1) to generali…
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first…
A Univalent Formalization of Constructive Affine Schemes
Max Zeuner, Anders Mörtberg
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucia…