Cauchy net > history in Homotopy Type Theory