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:

category: people