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         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 0̄) ≡ f (cons s 1̄))
    claim = Lemma[₂Fin-decidability] n
              (λ s → f (cons s 0̄) ≡ f (cons s 1̄))
              (λ s → ℕ-discrete (f (cons s 0̄)) (f (cons s 1̄)))
    sc₀ : ((s : ₂Fin n) → f (cons s 0̄) ≡ f (cons s 1̄)) →
          (α β : ₂ℕ) → α ≡[ 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 0̄
          claim₀ = ≡[succ] (Lemma[≡[]-cons-take] n)
                           (eα₀ · (Lemma[cons-take-0] n))
          claim₁ : f α ≡ f (cons s 0̄)
          claim₁ = a α (cons s 0̄) claim₀
          claim₂ : β ≡[ succ n ] cons s 1̄
          claim₂ = ≡[succ] (Lemma[≡[]-≡[]-take] n en)
                           (eβ₁ · (Lemma[cons-take-0] n))
          claim₃ : f β ≡ f (cons s 1̄)
          claim₃ = a β (cons s 1̄) 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 1̄
          claim₀ = ≡[succ] (Lemma[≡[]-cons-take] n)
                           (eα₁ · (Lemma[cons-take-0] n))
          claim₁ : f α ≡ f (cons s 1̄)
          claim₁ = a α (cons s 1̄) claim₀
          claim₂ : β ≡[ succ n ] cons s 0̄
          claim₂ = ≡[succ] (Lemma[≡[]-≡[]-take] n en)
                           (eβ₀ · (Lemma[cons-take-0] n))
          claim₃ : f β ≡ f (cons s 0̄)
          claim₃ = a β (cons s 0̄) claim₂
    sc₀' : (∀(s : ₂Fin n) → f (cons s 0̄) ≡ f (cons s 1̄))
         → decidable (∀(α β : ₂ℕ) → α ≡[ m ] β → f α ≡ f β)
    sc₀' ps = Uc-≤-decidable f n (sc₀ ps) m r'
    sc₁ : ¬ (∀(s : ₂Fin n) → f (cons s 0̄) ≡ f (cons s 1̄)) →
          ¬ (∀(α β : ₂ℕ) → α ≡[ m ] β → f α ≡ f β)
    sc₁ fs pn = fs (λ s → pn (cons s 0̄) (cons s 1̄) (Lemma[cons-≡[]-≤] s r'))
    sc₁' : ¬ (∀(s : ₂Fin n) → f (cons s 0̄) ≡ f (cons s 1̄)) →
           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}