Refactor inhabited, totally bounded metric spaces#1993

lowasser wants to merge 1 commit into

UniMath:masterUniMath/agda-unimath:masterfrom

lowasser:refactor-inhabited-totally-boundedlowasser/agda-unimath:refactor-inhabited-totally-boundedCopy head branch name to clipboard