definitional equality > history in Homotopy Type Theory