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
A formal proof of Sasaki-Murao algorithm	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 \textsc{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