Chuangjie Xu 2014 (updated in February 2015)


The type family UC(f) : ℕ → Set, defined by

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

satisfies

(1) Uc(f,n) is a proposition for all n (using funext), and

(2) if Uc(f,n) holds then Uc(f,m) is decidable for all m < n.


\begin{code}

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

module Continuity.DecidabilityOfUC where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Preliminaries.Boolean
open import Preliminaries.Sequence


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


Uc-hprop : Funext  (f : ₂ℕ  )   n  hprop (Uc f n)
          --------
Uc-hprop funext f n p q =
  funext  α  funext  β  funext  e  ℕ-hset (p α β e) (q α β e))))
 --------      --------      --------


Uc-≤-decidable : ∀(f : ₂ℕ  )   n  Uc f n
                 m  m  n  decidable (Uc f m)
Uc-≤-decidable f  0       a _ _ = inl  α β _  a α β ≡[zero])
Uc-≤-decidable f (succ n) a m r = case c₀ c₁ (Lemma[n≤m+1→n≤m∨n≡m+1] r)
 where
  c₀ : m  n  decidable (Uc f m)
  c₀ r' = case sc₀' sc₁' claim
   where
    claim : decidable ((s : ₂Fin n)  f (cons s )  f (cons s ))
    claim = Lemma[₂Fin-decidability] n
               s  f (cons s )  f (cons s ))
               s  ℕ-discrete (f (cons s )) (f (cons s )))
    sc₀ : ((s : ₂Fin n)  f (cons s )  f (cons s )) 
          (α β : ₂ℕ)  α ≡[ n ] β  f α  f β
    sc₀ efs α β en = case ssc₀ ssc₁ (₂-discrete (α n) (β n))
     where
      ssc₀ : α n  β n  f α  f β
      ssc₀ e = a α β (≡[succ] en e)
      ssc₁ : ¬ (α n  β n)  f α  f β
      ssc₁ ne = case sssc₀ sssc₁ Lemma[b≡₀∨b≡₁]
       where
        s : ₂Fin n
        s = take n α
        sssc₀ : α n    f α  f β
        sssc₀ eα₀ = claim₁ · (efs s) · claim₃ ⁻¹
         where
          eβ₁ : β n  
          eβ₁ = Lemma[b≠₀→b≡₁]  eβ₀  ne (eα₀ · eβ₀ ⁻¹))
          claim₀ : α ≡[ succ n ] cons s 
          claim₀ = ≡[succ] (Lemma[≡[]-cons-take] n)
                           (eα₀ · (Lemma[cons-take-0] n))
          claim₁ : f α  f (cons s )
          claim₁ = a α (cons s ) claim₀
          claim₂ : β ≡[ succ n ] cons s 
          claim₂ = ≡[succ] (Lemma[≡[]-≡[]-take] n en)
                           (eβ₁ · (Lemma[cons-take-0] n))
          claim₃ : f β  f (cons s )
          claim₃ = a β (cons s ) claim₂
        sssc₁ : α n    f α  f β
        sssc₁ eα₁ = claim₁ · (efs s)⁻¹ · claim₃ ⁻¹
         where
          eβ₀ : β n  
          eβ₀ = Lemma[b≠₁→b≡₀]  eβ₁  ne (eα₁ · eβ₁ ⁻¹))
          claim₀ : α ≡[ succ n ] cons s 
          claim₀ = ≡[succ] (Lemma[≡[]-cons-take] n)
                           (eα₁ · (Lemma[cons-take-0] n))
          claim₁ : f α  f (cons s )
          claim₁ = a α (cons s ) claim₀
          claim₂ : β ≡[ succ n ] cons s 
          claim₂ = ≡[succ] (Lemma[≡[]-≡[]-take] n en)
                           (eβ₀ · (Lemma[cons-take-0] n))
          claim₃ : f β  f (cons s )
          claim₃ = a β (cons s ) claim₂
    sc₀' : (∀(s : ₂Fin n)  f (cons s )  f (cons s ))
          decidable (∀(α β : ₂ℕ)  α ≡[ m ] β  f α  f β)
    sc₀' ps = Uc-≤-decidable f n (sc₀ ps) m r'
    sc₁ : ¬ (∀(s : ₂Fin n)  f (cons s )  f (cons s )) 
          ¬ (∀(α β : ₂ℕ)  α ≡[ m ] β  f α  f β)
    sc₁ fs pn = fs  s  pn (cons s ) (cons s ) (Lemma[cons-≡[]-≤] s r'))
    sc₁' : ¬ (∀(s : ₂Fin n)  f (cons s )  f (cons s )) 
           decidable (∀(α β : ₂ℕ)  α ≡[ m ] β  f α  f β)
    sc₁' fs = inr (sc₁ fs)
  c₁ : m  succ n  decidable (Uc f m)
  c₁ e = inl (transport (Uc f) (e ⁻¹) a)

\end{code}