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)

On ordinary cohomology in homotopy type theory:

category: people

Last revised on June 15, 2022 at 13:06:15. See the history of this page for a list of all contributions to it.