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/