Contents

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:

Last revised on January 14, 2021 at 06:46:37. See the history of this page for a list of all contributions to it.