• silent_water [she/her]@hexbear.net
    link
    fedilink
    English
    arrow-up
    1
    ·
    1 year ago

    there actually is a way to represent the reals with full generality in homotopy type theory – work is still on-going to implement it in a real programming language/prove type checking is decidable, but the theory is already in place – via Cauchy sequences.