infinite decimal representation of a unit interval > history in Homotopy Type Theory