Chuangjie Xu 2014

\begin{code}

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

module UsingFunext.Space.IndiscreteSpace where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage
open import UsingFunext.Space.Space
open import UsingFunext.Space.CartesianClosedness
open import UsingFunext.Space.Coproduct

\end{code}

Indisrecte C-spaces

\begin{code}

indiscrete : Space → Set
indiscrete X = ∀(p : ₂ℕ → U X) → p ∈ Probe X

\end{code}

The arbitrary product of indiscrete spaces is indiscrete.

\begin{code}

Proposition[∏-indiscrete] :

  ∀{I : Set} (X : I → Space) → (∀ i → indiscrete (X i)) → indiscrete (∏ X)

Proposition[∏-indiscrete] X indX p = goal
 where
  goal : p ∈ Probe (∏ X)
      -- ∀ i → (λ α → p α i) ∈ Probe (X i)
  goal i = indX i (λ α → p α i)

\end{code}

The coproduct of countable family of indiscrete spaces is indiscrete, if UC
holds in Set.

\begin{code}

Proposition[UC-∐-indiscrete] : Axiom[UC-ℕ] →

  ∀(X : ℕ → Space) → (∀(i : ℕ) → indiscrete (X i)) → indiscrete (∐ X)

Proposition[UC-∐-indiscrete] uc X indX p = n , prf
 where
  claim₀ : locally-constant (pr₁ ∘ p)
  claim₀ = uc (pr₁ ∘ p)
  n : ℕ
  n = pr₁ claim₀
  claim₁ : ∀(α β : ₂ℕ) → α ≡[ n ] β → pr₁(p α) ≡ pr₁(p β)
  claim₁ = pr₁ (pr₂ claim₀)
  prf : ∀(s : ₂Fin n) → Σ \(i : ℕ) → Σ \(q : ₂ℕ → U(X i)) →
          (q ∈ Probe (X i)) × (∀(α : ₂ℕ) → p(cons s α) ≡ (i , q α))
  prf s = i , q , sclaim₀ , sclaim₁
   where
    i : ℕ
    i = pr₁(p(cons s 0̄))
    e₀ : ∀(α : ₂ℕ) → pr₁(p(cons s α)) ≡ i
    e₀ α = claim₁ (cons s α) (cons s 0̄) (Lemma[cons-≡[]] s α 0̄)
    q : ₂ℕ → U(X i)
    q α = transport (U ∘ X) (e₀ α) (pr₂(p(cons s α)))
    sclaim₀ : q ∈ Probe(X i)
    sclaim₀ = indX i q
    sclaim₁ : ∀(α : ₂ℕ) → p(cons s α) ≡ (i , q α)
    sclaim₁ α = pair⁼ (e₀ α) refl

\end{code}