# * There Are No Discontinuous Real Functions *

## by Mark Bickford, Vincent Rahli

2014

Brouwer stated a continuity principle (CP) for total functionals

that map functions (int -> int) to numbers (int).

There are various ways to state CP in type theory.

As recently shown by Bauer and Escardo, some versions of CP are inconsistent with type theory (i.e. using them we can prove False).

However, using the Nuprl in Coq model, Vincent Rahli has just finished proving that a "squashed" version of CP

is true in Nuprl's type theory.

Since the "squashed" version of CP is weaker, what can we use it for?

Using Bishop's definition of the constructive real numbers, and given a function f of type Real -> Real, and a real number x, we can not prove that f is continuous at x,but we can prove that f is not discontinuous at x!

In the seminar we will go through Escardo's proof that the strong CP is false (in any type theory like Nuprl, Coq, or Agda). Then Vincent will discuss how he showed that the squashed CP is true in Nuprl, and Mark will discuss how that can be used to prove that there are no

discontinuous real functions.