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.


{-# 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


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


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

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


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).


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)


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.


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)