ETCS with elements > history in Homotopy Type Theory