High-logic stuff here. I don't claim to understand all but the
'gist'. The gist: HoTT is attempting to become THE foundation
for mathematics via Logic. Like... THE. There's been other
attempts in the past and likely to be others in the future, but
HoTT is.. hot stuff in this particular field. Since Theoretical
Physics is founded upon mathematics (to hopefully find
confirmation in reality), a reformulation of the foundations
(universals of logic) of the foundation (mathematics, which is
really founded on geometry but then again, geometry is founded
on the axiom/proof system, which goes back to logic) of the
foundation (Theoretical Physics) of Physics, which is supposed
to be the foundation all physical systems WHICH is supposed to
be the foundations of Reality itself.... the effort is worth it.
So foundation. Much reductive everythingness. I love this
article for the Title more than anything else and knowing what
they're attempting to do. Personally? I think they'll end up
chasing complicated tails around and still be missing the cheese
and the maze, but we'll definitely learn a LOT in the process of
going through it all. Above my head? Yup. I couldn't do it. But
I've got an intuition for accuracy without the refinements of
precision. I'd rather be accurate than overly precise because
too much precision towards the wrong bulleye can lead you to be
perfect and perfectly wrong at the same time. So, I try to avoid
that. Gives me headaches. But I admire those who strive for
precision with all my admirative abilities BECAUSE they're doing
what I can't or won't, and I cheer them all, while also
maintaining my own ignorance of things-very-precise. For me,
they'd be mazes I'd have trouble getting out of.
[1]
http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/
References
Visible links
1.
http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/