Homotopy Type Theory (HoTT), developed recently in a large collaboration centered at IAS, Princeton, combines elements from type theory, logic and topology to give alternative foundations of mathematics which are much closer to mathematical practice (useful for Automated Reasoning). HoTT also gives new insights into topology.