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