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:

On computing the first stable homotopy group of spheres via homotopy type theory (“Brunerie number”) with cubical Agda:

category: people

Last revised on July 13, 2024 at 08:45:52. See the history of this page for a list of all contributions to it.