Chuangjie Xu & Martin Escardo 2015

One of Brouwer's continuity principles is the following

    All functions ₂ℕ → ℕ are uniformly continuous

whose logical formulation is

    ∀(f : ₂ℕ → ℕ). ∃(m : ℕ). ∀(α,β : ₂ℕ). α =[m] β → f α = f β

where α =[m] β expresses that the sequences α and β agree up to the
first m positions.

\begin{code}

{-# OPTIONS --without-K #-}

module Continuity.EquivalentFormulationsOfUC where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.DecidabilityOfUC
open import Continuity.MainLemmas
open import Continuity.PropositionalTruncation
open import Continuity.TheoremKECA

\end{code}

We postulate (a weaker form of) propositional truncations, and have
the following formulations of uniform continuity principle.

\begin{code}

UC : Set
UC = (f : ₂ℕ → ℕ) → ∥ (Σ \(n : ℕ) → ∀(α β : ₂ℕ) → α ≡[ n ] β → f α ≡ f β) ∥

CH-UC : Set
CH-UC = (f : ₂ℕ → ℕ) → Σ \(n : ℕ) → ∀(α β : ₂ℕ) → α ≡[ n ] β → f α ≡ f β

\end{code}

For any type family A : ℕ → U such that

  (1) A(n) is a proposition for all n,

  (2) if A(n) then A(m) is decidable for all i < n,

we have

    ∥ Σ(n:ℕ).A(n) ∥ → Σ(n:ℕ).A(n).

\begin{code}

MainLemma : {A : ℕ → Set} →
            (dA : ∀ n → A n → ∀ i → i ≤ n → decidable (A i)) →
            (∀ n → hprop (A n))
          → ∥ (Σ \(n : ℕ) → A n) ∥ → Σ \(n : ℕ) → A n
MainLemma dA hA = Theorem[KECA-TLCA'2013] (μ dA) (μ-constant dA hA)

\end{code}

Since Uc(f) : ℕ → U, defined by

  Uc(f,n) = (α β : ₂ℕ) → α ≡[ n ] β → f α ≡ f β

satisfies (1) and (2), with the aid of (funext), the two formulations
of uniform continuity principles are logically equivalent.

\begin{code}

Theorem[CH-UC→UC] : CH-UC → UC
Theorem[CH-UC→UC] chuc = λ f → ∣ chuc f ∣

Theorem[UC→CH-UC] : Funext → UC → CH-UC
Theorem[UC→CH-UC] funext uc =
    λ f → MainLemma (Uc-≤-decidable f) (Uc-hprop funext f) (uc f)
                                                --------

\end{code}