nLab
Anders Mörtberg

Selected writings

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

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)
category: people

Last revised on January 6, 2021 at 03:24:31. See the history of this page for a list of all contributions to it.