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 Univalent Foundations" (https://arxiv.org/pdf/1210.5658.pdf) 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
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
