Dedekind cut structure > history in Homotopy Type Theory