[slack3r]

I wouldn't say it "challenges" set theory.

For this to be the case there have to demonstrable advantages over working with set theory. The main attraction of HoTT is that it allows people to do homotopy theory on computers using theorem provers. It is still a very open question whether this is an improvement over pen and paper math. It's still not clear if HoTT is just some neat technical gimmick that allows one to model homotopy theory using type theory.

This is still certainly worth investigating, but saying that HoTT "subsumes" set theory is a bit strong.

I would refer the interested reader to the discussion at https://mathematicswithoutapologies.wordpress.com/2015/05/13... (between Jacob Lurie, Shulman and Voevodsky).