nLab Anders Mörtberg

• webpage

Selected writings

On affine schemes in cubical type theory:

• Anders Mörtberg, Max Zeuner, A Univalent Formalization of Affine Schemes (arXiv:2212.02902)

Introducing the programming language Cubical Agda implementing univalent cubical homotopy type theory with higher inductive types:

• Anders Mörtberg, Cubical Agda (2018) [blog post]

• Andrea Vezzosi, Anders Mörtberg, Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, Proceedings of the ACM on Programming Languages 3 ICFP 87 (2019) 1–29 [doi:10.1145/3341691, pdf]

On cubical homotopy type theory implemented in the proof assistant Cubical Agda:

• Anders Mörtberg, Cubical methods in HoTT/UF, 2019 (pdf)

Exposition in view of synthetic homotopy theory:

• Anders Mörtberg, Loïc Pujet, Cubical synthetic homotopy theory, CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (Jan 2020) 158–171 [doi:10.1145/3372885.3373825, pdf]

On ordinary cohomology in homotopy type theory:

• Guillaume Brunerie, Axel Ljungström, Anders Mörtberg, Synthetic Integral Cohomology in Cubical Agda, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) 216 (2022) $[$doi:10.4230/LIPIcs.CSL.2022.11$]$

  (in cubical Agda)

On computing the first stable homotopy group of spheres via homotopy type theory (“Brunerie number”) with cubical Agda:

• Anders Mörtberg: Computational Proofs in Synthetic Homotopy Theory, talk at Running HoTT 2024, CQTS@NYUAD (April 2024) [video:kt]

Related entries

• cubical type theory

category: people