Homotopy Type Theory: The Logic of Space