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)

Related $n$Lab entries

• cubical type theory

category: people