We work constructively in HoTT/UF.
Let ℕ∞ be the type of conatural numbers, which extends ℕ with a point at infinity.
The type ℕ∞ has decidable equality iff WLPO holds.
However, for every n : ℕ and x : ℕ∞, it is decidable whether n ＝ x. We say that the finite elements of ℕ∞ are "isolated".
An intuition for a general element of ℕ∞ is as the behaviour of a stopwatch that either ticks finitely many times and then stops, or else ticks forever if nobody bothers to stop it.
With this intuition, define x ＝ₘ y, for x y : ℕ∞, to mean that we can't distinguish x and y after only m ticks. I am sure you can make this formal if you want to.
I will abuse language and regard any n : ℕ as an element of ℕ∞ by ticking n times and then stopping.
Let f : ℕ∞ → ℕ be any function.
There are (at least) six senses in which f can be considered to be continuous.
(1) ∃ m ꞉ ℕ , (Π n : ℕ , f (max m n) ＝ f ∞).
(1') Σ m ꞉ ℕ , (Π n : ℕ , f (max m n) ＝ f ∞).
(2) Π x : ℕ∞ , ∃ m ꞉ ℕ , (Π y : ℕ∞ , x ＝ₘ y → f x ＝ f y).
(2') Π x : ℕ∞ , Σ m ꞉ ℕ , (Π y : ℕ∞ , x ＝ₘ y → f x ＝ f y).
(3) ∃ m ꞉ ℕ , (Π x y : ℕ∞ , x ＝ₘ y → f x ＝ f y).
(3') Σ m ꞉ ℕ , (Π x y : ℕ∞ , x ＝ₘ y → f x ＝ f y).
Perhaps surprisingly, they are all logically equivalent, constructively, without the need for Brouwerian intuitionistic axioms.
(1) continuity property at ∞.
(1') continuity data at ∞.
(2) continuity property at all points
(2') continuity data at all points.
(3) uniform continuity property at all points.
(3') uniform continuity data all points.
If you want to see formal definitions, statements and proofs, here they are:
https://www.cs.bham.ac.uk/~mhe/TypeTopology/TypeTopology.DecidabilityOfNonContinuity.html
1/
