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}