nLab
mathematics presented in homotopy type theory

Contents

Context

Foundations

Mathematics

Contents

Idea

Homotopy type theory is a formal language in which it is possible to carry out synthetic mathematics using proof assistants, such as Coq and Agda. This is also possible in extensions to modal homotopy type theory.

Existing work

Homotopy type theory

Work conducted in homotopy type theory:

Construction of the quaternionic Hopf fibration

Work which uses modal homotopy type theory, with, for example, modalities for cohesion, differential cohesion and supergeometry:

See also Some thoughts on the future of modal homotopy type theory.

Last revised on July 8, 2019 at 04:28:46. See the history of this page for a list of all contributions to it.