Anders Mörtberg

Available identifiers

zbMath Open mortberg.andersMaRDI QIDQ2319989

List of research outcomes

Publication	Date of Publication	Type
A univalent formalization of constructive affine schemes	2024-11-26	Paper
https://portal.mardi4nfdi.de/entity/Q6124941	2024-04-10	Paper
Unifying Cubical Models of Univalent Type Theory	2023-02-07	Paper
Formalizing $\pi_4(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$ and Computing a Brunerie Number in Cubical Agda	2023-01-31	Paper
Cubical methods in homotopy type theory and univalent foundations	2022-12-09	Paper
Computing Cohomology Rings in Cubical Agda	2022-12-08	Paper
A Univalent Formalization of Constructive Affine Schemes	2022-12-06	Paper
Cubical Agda: A dependently typed programming language with univalence and higher inductive types	2021-12-13	Paper
Implementing a Category-Theoretic Framework for Typed Abstract Syntax	2021-12-13	Paper
On Higher Inductive Types in Cubical Type Theory	2021-01-20	Paper
https://portal.mardi4nfdi.de/entity/Q5195247	2019-09-18	Paper
From signatures to monads in \textsf{UniMath}	2019-08-21	Paper
Cubical Type Theory: a constructive interpretation of the univalence axiom	2018-08-13	Paper
Some Wellfounded Trees in UniMath	2016-09-28	Paper
Formalized linear algebra over Elementary Divisor Rings in Coq	2016-07-06	Paper
Computing persistent homology within Coq/SSReflect	2015-09-17	Paper
Refinements for Free!	2015-01-13	Paper
A Coq Formalization of Finitely Presented Modules	2014-09-08	Paper
Coherent and Strongly Discrete Rings in Type Theory	2013-04-19	Paper
A Refinement-Based Approach to Computational Algebra in Coq	2012-09-20	Paper
Towards a Certified Computation of Homology Groups for Digital Images	2012-07-23	Paper
Computational Synthetic Cohomology Theory in Homotopy Type Theory	N/A	Paper
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations	N/A	Paper

Research outcomes over time

This page was built for person: Anders Mörtberg