nLab Anders Mörtberg

• webpage

Selected writings

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

• Andrea Vezzosi, Anders Mörtberg and Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, 2019 (pdf)

• 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 January 2020, pp. 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)

Related $n$Lab entries

• cubical type theory

category: people