natural transformation > history in Homotopy Type Theory