Warning: Some posts on this platform may contain adult material intended for mature audiences only. Viewer discretion is advised. By clicking ‘Continue’, you confirm that you are 18 years or older and consent to viewing explicit content.
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.
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.