discrete GCD domain > history in Homotopy Type Theory