\begin{code}
{-# OPTIONS --without-K #-}
module UsingSetoid.Space.DiscreteSpace where
open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness
\end{code}
\begin{code}
Setoid≡ : Set → Setoid
Setoid≡ X = X , _≡_ , ≡-isEqRel
LC : {X : Set} → E-map-₂ℕ (Setoid≡ X) → Set
LC (f , _) = locally-constant f
LC-topology : (X : Set) → discrete X → probe-axioms (Setoid≡ X) LC
LC-topology X dis = c₀ , c₁ , c₂ , c₃
where
SX : Setoid
SX = Setoid≡ X
c₀ : ∀(x : X) → E-λα SX x ∈ LC
c₀ x = 0 , (λ _ _ _ → refl) , (λ _ _ → ≤-zero)
c₁ : ∀ t → t ∈ C → ∀ p → p ∈ LC → ⟨ SX ⟩ p ◎ t ∈ LC
c₁ (t , et) uc (p , ep) (m , pr , _) =
Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ (p ∘ t) n claim₁
where
n : ℕ
n = pr₁ (uc m)
claim₀ : ∀(α β : ₂ℕ) → α ≡[ n ] β → t α ≡[ m ] t β
claim₀ = pr₁ (pr₂ (uc m))
claim₁ : ∀(α β : ₂ℕ) → α ≡[ n ] β → p(t α) ≡ p(t β)
claim₁ α β en = pr (t α) (t β) (claim₀ α β en)
c₂ : ∀ p → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ SX ⟩ p ◎ Cons s ∈ LC) → p ∈ LC
c₂ (p , ep) (n , ps) = Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ p (n + k) prf
where
f : ₂Fin n → ℕ
f s = pr₁ (ps s)
k : ℕ
k = pr₁ (max-fin f)
k-max : ∀(s : ₂Fin n) → f s ≤ k
k-max = pr₂ (max-fin f)
fact : ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → α ≡[ k ] β → p(cons s α) ≡ p(cons s β)
fact s α β ek = pr₁ (pr₂ (ps s)) α β (Lemma[≡[]-≤] ek (k-max s))
prf : ∀(α β : ₂ℕ) → α ≡[ n + k ] β → p α ≡ p β
prf α β enk = goal
where
s : ₂Fin n
s = take n α
en : α ≡[ n ] β
en = Lemma[≡[]-≤] enk (Lemma[a≤a+b] n k)
eqs : take n α ≡ take n β
eqs = Lemma[≡[]-take] en
α' : ₂ℕ
α' = drop n α
eα : cons s α' ≣ α
eα = Lemma[cons-take-drop] n α
β' : ₂ℕ
β' = drop n β
eβ : cons s β' ≣ β
eβ i = transport (λ x → cons x β' i ≡ β i)
(eqs ⁻¹) (Lemma[cons-take-drop] n β i)
awk : ∀(i : ℕ) → i < k → α' i ≡ β' i
awk i i<k = eqα · subgoal · eqβ ⁻¹
where
i+n<k+n : i + n < k + n
i+n<k+n = Lemma[a<b→a+c<b+c] i k n i<k
i+n<n+k : i + n < n + k
i+n<n+k = transport (λ m → (i + n) < m) (Lemma[n+m=m+n] k n) i+n<k+n
subgoal : α (i + n) ≡ β (i + n)
subgoal = Lemma[≡[]-<] enk (i + n) i+n<n+k
le : (n i : ℕ) → (α : ₂ℕ) → drop n α i ≡ α (i + n)
le 0 i α = refl
le (succ n) i α = le n i (α ∘ succ)
eqα : α' i ≡ α (i + n)
eqα = le n i α
eqβ : β' i ≡ β (i + n)
eqβ = le n i β
ek : α' ≡[ k ] β'
ek = Lemma[<-≡[]] awk
claim₀ : p α ≡ p(cons s α')
claim₀ = ep _ _ (λ i → (eα i)⁻¹)
claim₁ : p(cons s α') ≡ p(cons s β')
claim₁ = fact s α' β' ek
claim₂ : p(cons s β') ≡ p β
claim₂ = ep _ _ eβ
goal : p α ≡ p β
goal = claim₀ · claim₁ · claim₂
c₃ : ∀ p q → p ∈ LC → (∀ α → pr₁ p α ≡ pr₁ q α) → q ∈ LC
c₃ (p , _) (q , _) (n , prf , min) ex = (n , prf' , min')
where
prf' : ∀(α β : ₂ℕ) → α ≡[ n ] β → q α ≡ q β
prf' α β en = (ex α)⁻¹ · prf α β en · ex β
min' : ∀ n' → ((α β : ₂ℕ) → α ≡[ n' ] β → q α ≡ q β) → n ≤ n'
min' n' prn' = min n' (λ α β en' → (ex α) · (prn' α β en') · (ex β)⁻¹ )
DiscreteSpace : (X : Set) → discrete X → Space
DiscreteSpace X dis = Setoid≡ X , LC , LC-topology X dis
Lemma[discreteness] : (X : Set) (dis : discrete X) (Y : Space)
→ ∀(f : E-map (Setoid≡ X) (U Y))
→ continuous (DiscreteSpace X dis) Y f
Lemma[discreteness] X _ Y f p (m , prf , _) = cond₂ Y _ (m , claim)
where
claim : ∀(s : ₂Fin m)
→ (⟨ U Y ⟩ (⟨ Setoid≡ X ∣ U Y ⟩ f ◎ p) ◎ Cons s) ∈ Probe Y
claim s = cond₃ Y _ _ (cond₀ Y y) claim₁
where
y : G Y
y = pr₁ f (pr₁ p (cons s 0̄))
claim₀ : ∀(α : ₂ℕ) → pr₁ p (cons s 0̄) ≡ pr₁ p (cons s α)
claim₀ α = prf (cons s 0̄) (cons s α) (Lemma[cons-≡[]] s 0̄ α)
claim₁ : ∀(α : ₂ℕ) → E (U Y) y (pr₁ f (pr₁ p (cons s α)))
claim₁ α = pr₂ f _ _ (claim₀ α)
\end{code}
\begin{code}
₂Space : Space
₂Space = DiscreteSpace ₂ ₂-discrete
Lemma[discrete-₂Space] : (X : Space) → ∀ f → continuous ₂Space X f
Lemma[discrete-₂Space] X f = Lemma[discreteness] ₂ ₂-discrete X f
continuous-if : (A : Space) → Map ₂Space (A ⇒ A ⇒ A)
continuous-if A = (IF , e-IF) , c-IF
where
_~_ : G A → G A → Set
_~_ = E (U A)
IF : ₂ → G (A ⇒ A ⇒ A)
IF b = (if-b , e-if-b) , c-if-b
where
if-b : G A → G (A ⇒ A)
if-b a₀ = (if-b-a₀ , e-if-b-a₀) , c-if-b-a₀
where
if-b-a₀ : G A → G A
if-b-a₀ a₁ = if b a₀ a₁
e-if-b-a₀ : ∀ a₁ a₁' → a₁ ~ a₁' → if b a₀ a₁ ~ if b a₀ a₁'
e-if-b-a₀ a₁ a₁' ea₁ = lemma b
where
lemma : ∀ i → if i a₀ a₁ ~ if i a₀ a₁'
lemma ₀ = Refl (U A) a₀
lemma ₁ = ea₁
c-if-b-a₀ : continuous A A (if-b-a₀ , e-if-b-a₀)
c-if-b-a₀ p pA = cond₃ A _ _ (lemma₀ b) (lemma₁ b)
where
f : ₂ → E-map-₂ℕ (U A)
f ₀ = E-λα (U A) a₀
f ₁ = p
lemma₀ : ∀(i : ₂) → f i ∈ Probe A
lemma₀ ₀ = cond₀ A a₀
lemma₀ ₁ = pA
lemma₁ : ∀ i → ∀ α → pr₁ (f i) α ~ if i a₀ (pr₁ p α)
lemma₁ ₀ α = Refl (U A) a₀
lemma₁ ₁ α = Refl (U A) (pr₁ p α)
e-if-b : ∀ a₀ a₀' → a₀ ~ a₀' → ∀ a₁ → if b a₀ a₁ ~ if b a₀' a₁
e-if-b a₀ a₀' ea₀ a₁ = lemma b
where
lemma : ∀ i → if i a₀ a₁ ~ if i a₀' a₁
lemma ₀ = ea₀
lemma ₁ = Refl (U A) a₁
c-if-b : continuous A (A ⇒ A) (if-b , e-if-b)
c-if-b p pA q qA t tC = cond₃ A _ _ (lemma₀ b) (lemma₁ b)
where
f : ₂ → E-map-₂ℕ (U A)
f ₀ = ⟨ U A ⟩ p ◎ t
f ₁ = q
lemma₀ : ∀ i → f i ∈ Probe A
lemma₀ ₀ = cond₁ A t tC p pA
lemma₀ ₁ = qA
lemma₁ : ∀ i → ∀ α → pr₁ (f i) α ~ if i (pr₁ p (pr₁ t α)) (pr₁ q α)
lemma₁ ₀ α = Refl (U A) (pr₁ p (pr₁ t α))
lemma₁ ₁ α = Refl (U A) (pr₁ q α)
e-IF : ∀ b b' → b ≡ b' → ∀ a₀ a₁ → if b a₀ a₁ ~ if b' a₀ a₁
e-IF b .b refl = Refl (U (A ⇒ A ⇒ A)) (IF b)
c-IF : continuous ₂Space (A ⇒ A ⇒ A) (IF , e-IF)
c-IF = Lemma[discrete-₂Space] (A ⇒ A ⇒ A) (IF , e-IF)
\end{code}
\begin{code}
ℕSpace : Space
ℕSpace = DiscreteSpace ℕ ℕ-discrete
Lemma[discrete-ℕSpace] : (X : Space) → ∀ f → continuous ℕSpace X f
Lemma[discrete-ℕSpace] X f = Lemma[discreteness] ℕ ℕ-discrete X f
continuous-succ : Map ℕSpace ℕSpace
continuous-succ = E-succ , c-succ
where
E-succ : E-map Eℕ Eℕ
E-succ = (succ , λ _ _ → ap succ)
c-succ : ∀ p → p ∈ LC → ⟨ Eℕ ∣ Eℕ ⟩ E-succ ◎ p ∈ LC
c-succ (p , ep) (n , prf , min) = n , prf' , min'
where
prf' : ∀(α β : ₂ℕ) → α ≡[ n ] β → succ (p α) ≡ succ (p β)
prf' α β en = ap succ (prf α β en)
min' : ∀(n' : ℕ) → (∀ α β → α ≡[ n' ] β → succ(p α) ≡ succ(p β)) → n ≤ n'
min' n' pr' = min n' (λ α β en' → succ-injective(pr' α β en'))
continuous-rec : (A : Space) → Map A ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A)
continuous-rec A = (REC , e-REC) , continuity-of-REC
where
_~_ : G A → G A → Set
_~_ = E (U A)
ū : G (ℕSpace ⇒ A ⇒ A) → ℕ → G A → G A
ū f n = pr₁ (pr₁ (pr₁ (pr₁ f) n))
ē : (f : G (ℕSpace ⇒ A ⇒ A)) → (n : ℕ)
→ ∀ a a' → a ~ a' → ū f n a ~ ū f n a'
ē f n = pr₂ (pr₁ (pr₁ (pr₁ f) n))
REC : G A → G ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A)
REC a = ((rec-a , e-rec-a) , c-rec-a)
where
rec-a : G (ℕSpace ⇒ A ⇒ A) → G (ℕSpace ⇒ A)
rec-a f = (rec-a-f , e-rec-a-f) , c-rec-a-f
where
rec-a-f : ℕ → G A
rec-a-f = rec a (ū f)
e-rec-a-f : ∀ n m → n ≡ m → rec a (ū f) n ~ rec a (ū f) m
e-rec-a-f n .n refl = Refl (U A) (rec a (ū f) n)
c-rec-a-f : continuous ℕSpace A (rec-a-f , e-rec-a-f)
c-rec-a-f = Lemma[discrete-ℕSpace] A (rec-a-f , e-rec-a-f)
e-rec-a : ∀ f f' → (∀ n b → ū f n b ~ ū f' n b)
→ ∀ n → rec a (ū f) n ~ rec a (ū f') n
e-rec-a f f' ef 0 = Refl (U A) a
e-rec-a f f' ef (succ n) = Trans (U A) _ _ _ claim₀ claim₁
where
claim₀ : rec a (ū f) (succ n) ~ ū f' n (rec a (ū f) n)
claim₀ = ef n (rec a (ū f) n)
claim₁ : ū f' n (rec a (ū f) n) ~ rec a (ū f') (succ n)
claim₁ = ē f' n _ _ (e-rec-a f f' ef n)
c-rec-a : continuous (ℕSpace ⇒ A ⇒ A) (ℕSpace ⇒ A) (rec-a , e-rec-a)
c-rec-a p pNAA q (n , qr , _) t uc = cond₂ A _ (n , prf)
where
rec-a-p : E-map-₂ℕ (U(ℕSpace ⇒ A))
rec-a-p = ⟨ U (ℕSpace ⇒ A ⇒ A) ∣ U (ℕSpace ⇒ A) ⟩ (rec-a , e-rec-a) ◎ p
rec-a-pt-q : E-map-₂ℕ (U A)
rec-a-pt-q = Exp ℕSpace A rec-a-p t q
prf : ∀(s : ₂Fin n) → ⟨ U A ⟩ rec-a-pt-q ◎ Cons s ∈ Probe A
prf s = cond₃ A _ _ (lemma qs0) claim
where
tsC : t ◎ Cons s ∈ C
tsC = Lemma[◎-UC] t uc (Cons s) (Lemma[cons-UC] s)
pts : E-map-₂ℕ (U (ℕSpace ⇒ A ⇒ A))
pts = ⟨ U (ℕSpace ⇒ A ⇒ A) ⟩ p ◎ (t ◎ Cons s)
f : ℕ → E-map-₂ℕ (U A)
f k = g k , eg k
where
g : ℕ → ₂ℕ → G A
g i α = rec a (ū (pr₁ pts α)) i
eg : ∀ i → ∀ α α' → α ≣ α' → g i α ~ g i α'
eg 0 _ _ _ = Refl (U A) a
eg (succ i) α α' eα = Trans (U A) _ _ _ claim₁ claim₂
where
claim₀ : g i α ~ g i α'
claim₀ = eg i α α' eα
claim₁ : g (succ i) α ~ ū (pr₁ pts α) i (g i α')
claim₁ = ē (pr₁ pts α) i _ _ claim₀
claim₂ : ū (pr₁ pts α) i (g i α') ~ g (succ i) α'
claim₂ = pr₂ pts _ _ eα _ _
lemma : ∀ k → f k ∈ Probe A
lemma 0 = cond₀ A a
lemma (succ k) = cond₃ A _ _ claim₁ claim₂
where
ptsk : E-map-₂ℕ (U (A ⇒ A))
ptsk = Exp ℕSpace (A ⇒ A) p (t ◎ Cons s) (E-λα Eℕ k)
claim₀ : ptsk ∈ Probe (A ⇒ A)
claim₀ = pNAA (E-λα Eℕ k) (cond₀ ℕSpace k) (t ◎ Cons s) tsC
ptskfk : E-map-₂ℕ (U A)
ptskfk = Exp A A ptsk (E-id E₂ℕ) (f k)
claim₁ : ptskfk ∈ Probe A
claim₁ = claim₀ (f k) (lemma k) (E-id E₂ℕ) Lemma[id-UC]
claim₂ : ∀ α → pr₁ ptskfk α ~ pr₁ (f (succ k)) α
claim₂ α = Refl (U A) (pr₁ ptskfk α)
qs0 : ℕ
qs0 = pr₁ q (cons s 0̄)
claim : ∀ α → pr₁ (f qs0) α ~ pr₁ rec-a-pt-q (cons s α)
claim α = pr₂ (pr₁ (rec-a (pr₁ pts α))) _ _
(qr _ _ (Lemma[cons-≡[]] s 0̄ α))
e-REC : ∀ a a' → a ~ a' → ∀ f n → rec a (ū f) n ~ rec a' (ū f) n
e-REC a a' ea f 0 = ea
e-REC a a' ea f (succ n) = ē f n _ _ (e-REC a a' ea f n)
continuity-of-REC : continuous A ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A) (REC , e-REC)
continuity-of-REC p pA q qNAA t tC u (n , ur , _) v vC = cond₂ A _ (n , prf)
where
rec-p : E-map-₂ℕ (U ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A))
rec-p = ⟨ U A ∣ U ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A) ⟩ (REC , e-REC) ◎ p
rec-pt-q : E-map-₂ℕ (U (ℕSpace ⇒ A))
rec-pt-q = Exp (ℕSpace ⇒ A ⇒ A) (ℕSpace ⇒ A) rec-p t q
rec-ptv-qv-u : E-map-₂ℕ (U A)
rec-ptv-qv-u = Exp ℕSpace A rec-pt-q v u
prf : ∀(s : ₂Fin n) → ⟨ U A ⟩ rec-ptv-qv-u ◎ Cons s ∈ Probe A
prf s = cond₃ A _ _ (lemma us0) claim
where
vsC : v ◎ Cons s ∈ C
vsC = Lemma[◎-UC] v vC (Cons s) (Lemma[cons-UC] s)
ptvs : E-map-₂ℕ (U A)
ptvs = ⟨ U A ⟩ p ◎ (t ◎ v ◎ Cons s)
qvs : E-map-₂ℕ (U (ℕSpace ⇒ A ⇒ A))
qvs = ⟨ U (ℕSpace ⇒ A ⇒ A) ⟩ q ◎ (v ◎ Cons s)
tvsC : t ◎ v ◎ Cons s ∈ C
tvsC = Lemma[◎-UC] t tC (v ◎ Cons s) vsC
f : ℕ → E-map-₂ℕ (U A)
f k = g k , eg k
where
g : ℕ → ₂ℕ → G A
g i α = rec (pr₁ ptvs α) (ū(pr₁ qvs α)) i
eg : ∀ i → ∀ α α' → α ≣ α' → g i α ~ g i α'
eg 0 α α' eα = pr₂ p _ _ (pr₂ t _ _ (pr₂ v _ _ (cons-E-map s _ _ eα)))
eg (succ i) α α' eα = Trans (U A) _ _ _ claim₁ claim₂
where
claim₀ : g i α ~ g i α'
claim₀ = eg i α α' eα
claim₁ : g (succ i) α ~ ū (pr₁ qvs α) i (g i α')
claim₁ = ē (pr₁ qvs α) i _ _ claim₀
claim₂ : ū (pr₁ qvs α) i (g i α') ~ g (succ i) α'
claim₂ = pr₂ qvs _ _ eα _ _
lemma : ∀ k → f k ∈ Probe A
lemma 0 = cond₁ A (t ◎ v ◎ Cons s) tvsC p pA
lemma (succ k) = cond₃ A _ _ claim₁ claim₂
where
qvsk : E-map-₂ℕ (U (A ⇒ A))
qvsk = Exp ℕSpace (A ⇒ A) q (v ◎ Cons s) (E-λα Eℕ k)
claim₀ : qvsk ∈ Probe (A ⇒ A)
claim₀ = qNAA (E-λα Eℕ k) (cond₀ ℕSpace k) (v ◎ Cons s) vsC
qvskfk : E-map-₂ℕ (U A)
qvskfk = Exp A A qvsk (E-id E₂ℕ) (f k)
claim₁ : qvskfk ∈ Probe A
claim₁ = claim₀ (f k) (lemma k) (E-id E₂ℕ) Lemma[id-UC]
claim₂ : ∀ α → pr₁ qvskfk α ~ pr₁ (f (succ k)) α
claim₂ α = Refl (U A) (pr₁ qvskfk α)
us0 : ℕ
us0 = pr₁ u (cons s 0̄)
claim : ∀ α → pr₁ (f us0) α ~ pr₁ rec-ptv-qv-u (cons s α)
claim α = pr₂ (pr₁ (pr₁ rec-pt-q (pr₁ v (cons s α)))) _ _
(ur _ _ (Lemma[cons-≡[]] s 0̄ α))
\end{code}