Proving Axiom Correct: Homotopy Type Theory

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

Proving Axiom Correct: Homotopy Type Theory

Tim Daly
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer