[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Proving Axiom Correct: Homotopy Type Theory

From: Tim Daly
Subject: [Axiom-developer] Proving Axiom Correct: Homotopy Type Theory
Date: Tue, 4 Apr 2017 22:20:26 -0400

There has been a "great merger" of the ideas of Type Theory,
Category Theory, and Proof Theory. There is an interpretation
of a result in one in terms of the other two.

There has recently been a fundamentally new area of mathematics
that merges ideas from those three areas with algebraic topology.
This area is called "Homotopy Type Theory". It appears to be a
"computable form of mathematics". 

This represents, as near as I can understand, a new theory
as fundamental as group theory. Axiom uses group theory as an
organizing scaffold for the algebra, giving it a clean structure.

Homotopy Type Theory (HoTT) looks like it could give Axiom a
second scaffold of Type Theory / Proof Theory for proving 
computational mathematics correct.

In particular, it seems that this "second Axiom scaffold", when the 
theorems and proofs are matched with the group theory scaffold,
will give Axiom a very firm foundation for computational

Like group theory, HoTT is a steep hill to climb. There is a book
(available as a free PDF from called 
Homotopy Type Theory: Univalent Foundations of Mathematics. 
It is the work of a large group of mathematician, published by the 
Institute for Advanced Study.

The HoTT book is an intimidating piece of reading if you're not
familiar with all of the areas. A more gentle introduction would be
Pelayo and Warren, "Homotopy Type Theory and Voevodsky's
Univalent Foundations" (

This is the very bleeding edge of computational mathematics
and should put Axiom in the very heart of the developments.
A computer algebra system with proven soundness would change
the whole field.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]