Homotopy Type Theory for mathematicians