nLab Anders Mörtberg

Selected writings

On affine schemes in cubical type theory:

Introducing the programming language Cubical Agda implementing univalent cubical homotopy type theory with higher inductive types:

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

Exposition in view of synthetic homotopy theory:

On ordinary cohomology in homotopy type theory:

category: people

Last revised on November 22, 2023 at 20:02:39. See the history of this page for a list of all contributions to it.