Dedekind cut (disambiguation) > history in Homotopy Type Theory