rational interval coalgebra > history in Homotopy Type Theory