decimal interval coalgebra > history in Homotopy Type Theory