sigma-continuous valuation > history in Homotopy Type Theory