Dedekind real numbers (disambiguation) > history in Homotopy Type Theory