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

mathematics.

Like group theory, HoTT is a steep hill to climb. There is a book

(available as a free PDF from HomotopyTypeTheory.org) 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

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.

Tim