From what I understand, Homotopy Type Theory is proposed as a new foundation of mathematics, and it supposed to be superior for use with computer aided proofs.
I am currently trying to understand the theory, but I am also curious as to what practical results of the theory are in terms of the proofs you generate.
When I look at the coq code that is part of the UniMath project, for example the basic group theory:
https://github.com/UniMath/UniMath/blob/master/UniMath/Foundations/hlevel2/algebra1a.v
it looks very similar to the coq code from any other coq project, for example the group theory from the galios-theory project:
https://code.google.com/p/coq-galois-theory/source/browse/trunk/src/modules/constructive_lib.v
I'm not sure if I'm missing the point here. Is the benefit of HOTT at a lower level than group theory, just in terms of defining primitives? Or is it at a higher level than group theory, dealing with more complicated types which get messy to represent in the usual way. What about the supposed "computational" nature of HOTT?
What are some side-by-side comparisons of proofs/definitions that illustrate the power of HOTT? It would be nice if the examples were comprehensible to someone with only an undergraduate degree in math.