nLab mathematics presented in homotopy type theory

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

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 April 6, 2024 at 17:24:40. See the history of this page for a list of all contributions to it.