Chuangjie Xu and Martin Escardo, December 2013


For any type family A : ℕ → U such that

  if A(n) holds than A(m) is decidable for all m < n,  (†)

we have the followings:

  (1) if A(n) holds then there exists a minimal m with A(m), and

  (2) if A is proposition-valued, then there exists a constant endomap
      of Σ(n:ℕ).A(n).

\begin{code}

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

module Continuity.MainLemmas where

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

\end{code}

If A : ℕ → U satisfies (†) then (Π(m≤n).¬A(m)) + (Σ(m≤n).A(m)).

\begin{code}

Lemma[≤-dec-∨] : {A : ℕ → Set} →
        ∀(n : ℕ) → (∀(m : ℕ) → m ≤ n → decidable (A m)) →
        (∀ m → m ≤ n → ¬(A m)) + (Σ \m → m ≤ n × A m)
Lemma[≤-dec-∨] {A} 0 dA = case c₀ c₁ (dA 0 ≤-zero)
 where
  c₀ : A 0 → (∀ m → m ≤ 0 → ¬(A m)) + (Σ \m → m ≤ 0 × A m)
  c₀ a0 = inr (0 , ≤-zero , a0)
  c₁ : ¬(A 0) → (∀ m → m ≤ 0 → ¬(A m)) + (Σ \(m : ℕ) → m ≤ 0 × A m)
  c₁ f0 = inl claim
   where
    claim : ∀ m → m ≤ 0 → ¬(A m)
    claim 0 ≤-zero = f0
    claim (succ m) ()
Lemma[≤-dec-∨] {A} (succ n) dA = case c₀ c₁ (dA (succ n) ≤-refl)
 where
  dA' : ∀(m : ℕ) → m ≤ n → decidable (A m)
  dA' m r = dA m (≤-r-succ r)
  c₀ : A(succ n) → (∀ m → m ≤ succ n → ¬(A m)) + (Σ \m → m ≤ succ n × A m)
  c₀ asn = inr (succ n , ≤-refl , asn)
  c₁ : ¬(A(succ n)) → (∀ m → m ≤ succ n → ¬(A m)) + (Σ \m → m ≤ succ n × A m)
  c₁ fsn = cases sc₀ sc₁ (Lemma[≤-dec-∨] n dA')
   where
    sc₀ : (∀ m → m ≤ n → ¬(A m)) → ∀ m → m ≤ succ n → ¬(A m)
    sc₀ fms m r = case (fms m) (λ e → transport (¬ ∘ A) (e ⁻¹) fsn)
                       (Lemma[n≤m+1→n≤m∨n≡m+1] r)
    sc₁ : (Σ \m → m ≤ n × A m) → Σ \m → m ≤ succ n × A m
    sc₁ (m , r , am) = (m , ≤-r-succ r , am)

\end{code}

If A : ℕ → U satisfies (†) then given A(n) one can find the minimal m
such that A(m) holds.

\begin{code}

private

 g : {A : Set} → A + ¬ A → A → A
 g (inl a) _ = a
 g (inr f) a = ∅-elim (f a)

 cg : {A : Set} → ∀(w : A + ¬ A) → constant (g w)
 cg (inl a) _ _ = refl
 cg (inr f) a _ = ∅-elim (f a)

Lemma[Σ-min] : {A : ℕ → Set} →
               (n : ℕ) → A n → (∀ i → i ≤ n → decidable (A i)) →
               Σ-min \(m : ℕ) → A m
Lemma[Σ-min] {A} = CoV-induction step
 where
  P : ℕ → Set
  P n = A n → (∀ i → i ≤ n → decidable (A i)) → Σ-min \(m : ℕ) → A m
  step : ∀ n → (∀ m → m < n → P m) → P n
  step 0        f a0  dA = 0 , g (dA 0 ≤-zero) a0 , (λ _ _ → ≤-zero)
  step (succ n) f asn dA = case c₀ c₁ claim
   where
    dA' : ∀(m : ℕ) → m ≤ n → decidable (A m)
    dA' m r = dA m (≤-r-succ r)
    claim : (∀ m → m ≤ n → ¬(A m)) + (Σ \m → m ≤ n × A m)
    claim = Lemma[≤-dec-∨] n dA'
    c₀ : (∀ m → m ≤ n → ¬(A m)) → Σ-min \(m : ℕ) → A m
    c₀ fm = succ n , g (dA (succ n) ≤-refl) asn , min
     where
      min : ∀ m → A m → succ n ≤ m
      min m am = Lemma[n≰m→m<n] (λ r → fm m r am)
    c₁ : (Σ \m → m ≤ n × A m) → Σ-min \(m : ℕ) → A m
    c₁ (m , r , am) = f m (≤-succ r) am dAm
     where
      dAm : ∀ k → k ≤ m → decidable (A k)
      dAm k r' = dA k (≤-trans r' (≤-r-succ r))

\end{code}

If A : ℕ → U is proposition-valued and satisfies (†) then there exists
a constant endomap of Σ(n:ℕ).A(n).

\begin{code}

μ : {A : ℕ → Set} →
    (∀ n → A n → ∀ i → i ≤ n → decidable (A i)) →
    (Σ \(n : ℕ) → A n) → Σ \(m : ℕ) → A m
μ dA (n , p) = re-pair (Lemma[Σ-min] n p (dA n p))

pr₁-μ-constant : {A : ℕ → Set} →
                 (dA : ∀ n → A n → ∀ i → i ≤ n → decidable (A i)) →
                 (w₀ w₁ : Σ \(n : ℕ) → A n)
               → pr₁(μ dA w₀) ≡ pr₁(μ dA w₁)
pr₁-μ-constant {A} dA (n₀ , p₀) (n₁ , p₁) = goal
 where
  m₀ : ℕ
  m₀ = pr₁(μ dA (n₀ , p₀))
  min₀ : ∀(k : ℕ) → A k → m₀ ≤ k
  min₀ = pr₂(pr₂(Lemma[Σ-min] n₀ p₀ (dA n₀ p₀)))
  q₀ : A m₀
  q₀ = pr₂(μ dA (n₀ , p₀))
  m₁ : ℕ
  m₁ = pr₁(μ dA (n₁ , p₁))
  min₁ : ∀(k : ℕ) → A k → m₁ ≤ k
  min₁ = pr₂(pr₂(Lemma[Σ-min] n₁ p₁ (dA n₁ p₁)))
  q₁ : A m₁
  q₁ = pr₂(μ dA (n₁ , p₁))
  goal : m₀ ≡ m₁
  goal = Lemma[m≤n∧n≤m→m=n] (min₀ m₁ q₁) (min₁ m₀ q₀)

μ-constant : {A : ℕ → Set} →
             (dA : ∀ n → A n → ∀ i → i ≤ n → decidable (A i)) →
             (∀ n → hprop (A n))
           → ∀(w₀ w₁ : Σ \(n : ℕ) → A n) → μ dA w₀ ≡ μ dA w₁
μ-constant {A} dA hA (n₀ , p₀) (n₁ , p₁) = pair⁼ e₀ e₁
 where
  m₀ : ℕ
  m₀ = pr₁(μ dA (n₀ , p₀))
  q₀ : A m₀
  q₀ = pr₂(μ dA (n₀ , p₀))
  m₁ : ℕ
  m₁ = pr₁(μ dA (n₁ , p₁))
  q₁ : A m₁
  q₁ = pr₂(μ dA (n₁ , p₁))
  e₀ : m₀ ≡ m₁
  e₀ = pr₁-μ-constant dA (n₀ , p₀) (n₁ , p₁)
  q₀' : A m₁
  q₀' = transport A e₀ q₀
  e₁ : q₀' ≡ q₁
  e₁ = hA m₁ q₀' q₁

\end{code}

If A(i) is decidable for all i : ℕ (without requiring A to be
proposition-valued), then there exists a constant endomap of
Σ(n:ℕ).A(n).

\begin{code}

μμ : {A : ℕ → Set} → (∀ i → decidable (A i)) →
     (Σ \(n : ℕ) → A n) → Σ \(m : ℕ) → A m
μμ {A} dA w = μ dA' (μ dA' w)
 where
  dA' : ∀ n → A n → ∀ i → i ≤ n → decidable (A i)
  dA' _ _ i _ = dA i

μμ-constant : {A : ℕ → Set} → (dA : ∀ i → decidable (A i)) →
              constant (μμ dA)
μμ-constant {A} dA = goal
 where
  dA' : ∀ n → A n → ∀ i → i ≤ n → decidable (A i)
  dA' _ _ i _ = dA i
  lemma₀ : ∀(n : ℕ) → ∀(a b : A n) → μ dA' (n , a) ≡ μ dA' (n , b)
  lemma₀ 0        a b = pair⁼ refl (cg (dA 0) a b)
  lemma₀ (succ n) a b = equality-cases claim c₀ c₁
   where
    claim : (∀ m → m ≤ n → ¬(A m)) + (Σ \m → m ≤ n × A m)
    claim = Lemma[≤-dec-∨] n (λ i r → dA i)
    c₀ : (t : ∀ m → m ≤ n → ¬(A m)) → claim ≡ inl t →
         μ dA' (succ n , a) ≡ μ dA' (succ n , b)
    c₀ t e = eq₀ · eq₂ · eq₁ ⁻¹
     where
      eq₀ : μ dA' (succ n , a) ≡ (succ n , g (dA (succ n)) a)
      eq₀ = Σ-min-≡ (ap (case _ _) e)
      eq₁ : μ dA' (succ n , b) ≡ (succ n , g (dA (succ n)) b)
      eq₁ = Σ-min-≡ (ap (case _ _) e)
      eq₂ : _≡_ {A = Σ A} (succ n , g (dA (succ n)) a)
                      (succ n , g (dA (succ n)) b)
      eq₂ = pair⁼ refl (cg (dA (succ n)) a b)
    c₁ : (u : Σ \m → m ≤ n × A m) → claim ≡ inr u →
         μ dA' (succ n , a) ≡ μ dA' (succ n , b)
    c₁ (m , r , _) e = Σ-min-≡ ((ap (case _ _) e) · (ap (case _ _) e)⁻¹)
  lemma₁ : ∀(w₀ w₁ : Σ \(n : ℕ) → A n) → pr₁ w₀ ≡ pr₁ w₁ → μ dA' w₀ ≡ μ dA' w₁
  lemma₁ (n , p₀) (.n , p₁) refl = lemma₀ n p₀ p₁
  goal : ∀(w₀ w₁ : Σ \(n : ℕ) → A n) → μμ dA w₀ ≡ μμ dA w₁
  goal w₀ w₁ = lemma₁ (μ dA' w₀) (μ dA' w₁) (pr₁-μ-constant dA' w₀ w₁)

\end{code}