jozefg/intrinsic.agda

## intrinsic.agda
module intrinsic where
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum as S
open import Data.Bool as B
open import Data.Nat as N
open import Data.Nat.Properties as NP

postulate fext : {A : Set}{B : A → Set}(f g : (a : A) → B a) → ((a : A) → f a ≡ g a) → f ≡ g

fold : {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
fold f g (inj₁ x) = f x
fold f g (inj₂ y) = g y

Σ-ext : {A : Set}{B : A → Set}{p q : Σ A B}(eq : proj₁ p ≡ proj₁ q) → subst B eq (proj₂ p) ≡ proj₂ q → p ≡ q
Σ-ext refl refl = refl

×-ext : {A B : Set}{p q : A × B} → proj₁ p ≡ proj₁ q → proj₂ p ≡ proj₂ q → p ≡ q
×-ext refl refl = refl

⊎-ext : {A B C : Set}{f g : A ⊎ B → C}
      → ((a : A) → f (inj₁ a) ≡ g (inj₁ a))
      → ((b : B) → f (inj₂ b) ≡ g (inj₂ b))
      → (s : A ⊎ B) → f s ≡ g s
⊎-ext l r (inj₁ x) = l x
⊎-ext l r (inj₂ y) = r y

bool-split : (b : Bool) → (b ≡ false) ⊎ (b ≡ true)
bool-split true = inj₂ refl
bool-split false = inj₁ refl

true≢false : true ≢ false
true≢false ()

bool-flip : {b1 b2 : Bool} → b1 ≢ b2 → b1 ≡ not b2
bool-flip {false} {false} eq = ⊥-elim (eq refl)
bool-flip {false} {true} eq = refl
bool-flip {true} {false} eq = refl
bool-flip {true} {true} eq = ⊥-elim (eq refl)

_≅_ : Set → Set → Set
A ≅ B = Σ (A → B) λ f → Σ (B → A) λ g → f ∘ g ≡ id × g ∘ f ≡ id

≅-refl : {A : Set} → A ≅ A
≅-refl = id , id , refl , refl

≅-sym : {A B : Set} → A ≅ B → B ≅ A
≅-sym (f , g , eq1 , eq2) = (g , f , eq2 , eq1)

≅-trans : {A B C : Set} → A ≅ B → B ≅ C → A ≅ C
≅-trans {A} {B} {C} (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
  (λ z → f2 (f1 z)) , (λ z → g1 (g2 z)) ,
  (fext _ _ eq1) , fext _ _ eq2
  where eq1 : (c : C) → f2 (f1 (g1 (g2 c))) ≡ c
        eq1 c rewrite cong-app eq11 (g2 c) | cong-app eq21 c = refl
        eq2 : (a : A) → g1 (g2 (f2 (f1 a))) ≡ a
        eq2 a rewrite cong-app eq22 (f1 a) | cong-app eq12 a = refl

⊥×-≅ : {A : Set} → (⊥ × A) ≅ ⊥
⊥×-≅ = proj₁ , (λ ()) , fext _ _ (λ ()) , fext _ _ λ p → ⊥-elim (proj₁ p)

⊤×-≅ : {A : Set} → (⊤ × A) ≅ A
⊤×-≅ = proj₂ , (λ a → tt , a) , refl , fext _ _ λ p → ×-ext refl refl

⊥⊤→-≅ : (⊤ → ⊥) ≅ ⊥
⊥⊤→-≅ = (λ z → z tt) , (λ z _ → z) , refl , fext _ _ λ a → ⊥-elim (a tt)

⊥⊥→-≅ : (⊥ → ⊥) ≅ ⊤
⊥⊥→-≅ = (λ _ → tt) , (λ _ z → z) , (fext _ _ λ x → refl) , fext _ _ λ x → fext _ _ λ ()

⊥⊎-≅ : {A : Set} → (⊥ ⊎ A) ≅ A
⊥⊎-≅ = fold ⊥-elim id , inj₂ , (fext _ _ λ a → refl) , fext _ _ (⊎-ext (λ ()) (λ b → refl))

⊎⊥-≅ : {A : Set} → (A ⊎ ⊥) ≅ A
⊎⊥-≅ = fold id ⊥-elim , inj₁ , (fext _ _ λ a → refl) , fext _ _ (⊎-ext (λ b → refl) (λ ()))

coerce : Bool → Set
coerce false = ⊤
coerce true = ⊥

ℕ∞ : Set
ℕ∞ = Σ (ℕ → Bool) λ f → (i : ℕ) → coerce (f i) → coerce (f (suc i))

evidence-triv : (f : ℕ → Bool)(a b : (i : ℕ) → coerce (f i) → coerce (f (suc i)))
              → a ≡ b
evidence-triv f a b = fext _ _ λ i → prf f i (a i) (b i)
  where prf : (f : ℕ → Bool)(i : ℕ)(a b : coerce (f i) → coerce (f (suc i))) → a ≡ b
        prf f i a b with f (suc i) | f i
        prf f i a b | p | true = fext _ _ λ ()
        prf f i a b | true | false = ⊥-elim (b tt)
        prf f i a b | false | false = fext _ _ λ _ → refl

ℕ∞-eq : (i j : ℕ∞) → proj₁ i ≡ proj₁ j → i ≡ j
ℕ∞-eq i j eq = Σ-ext eq (evidence-triv _ _ _)

raw-nat : ℕ → ℕ → Bool
raw-nat upper n with n NP.<? upper
... | yes _ = true
... | no _ = false

nat : ℕ → ℕ∞
nat n = raw-nat n , prf n
  where prf : (n : ℕ)(i : ℕ) → coerce (raw-nat n i) → coerce (raw-nat n (suc i))
        prf n i p with i NP.<? n
        prf n i () | yes p₁
        prf n i p | no ¬p with suc i NP.<? n
        prf n i p | no ¬p | yes q = ¬p (≤-trans (n≤1+n (suc i)) q)
        prf n i p | no ¬p | no _ = tt

raw-nat-inj : (n m : ℕ) → raw-nat n ≡ raw-nat m → n ≡ m
raw-nat-inj n m eq with N.compare n m
raw-nat-inj n .(suc (n + k)) eq | less .n k with cong-app eq n
... | eq' with n NP.<? n | n NP.<? suc (n + k)
... | yes p | _ = ⊥-elim (1+n≰n p)
raw-nat-inj n .(suc (n + k)) eq | less .n k | () | no ¬p | yes p
... | no _ | no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))
raw-nat-inj n .n eq | equal .n = refl
raw-nat-inj .(suc (m + k)) m eq | greater .m k with cong-app eq m
... | eq' with m NP.<? m | m NP.<? suc (m + k)
... | yes p | _ = ⊥-elim (1+n≰n p)
raw-nat-inj .(suc (m + k)) m eq | greater .m k | () | no ¬p | yes p
... | no _ | no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))

nat-inj : (n m : ℕ) → nat n ≡ nat m → n ≡ m
nat-inj n m eq = raw-nat-inj n m (cong proj₁ eq)

inf : ℕ∞
inf = (λ _ → true), (λ i ())

inf-not-nat : (n : ℕ) → nat n ≢ inf
inf-not-nat n eq with cong-app (cong proj₁ eq) (suc n)
inf-not-nat n eq | p with suc n NP.<? n
inf-not-nat n eq | p | yes p₁ = ⊥-elim (1+n≰n (≤-trans (n≤1+n (suc n)) p₁))
inf-not-nat n eq | () | no ¬p

false-extends-up-one : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ false → proj₁ i (suc n) ≡ false
false-extends-up-one (s , prf) n eq with prf n | bool-split (s (suc n))
false-extends-up-one (s , prf) n eq | p | inj₁ q = q
false-extends-up-one (s , prf) n eq | p | inj₂ q rewrite eq | q = ⊥-elim (p tt)

false-extends-up : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ false
                 → (m : ℕ) → n N.≤ m → proj₁ i m ≡ false
false-extends-up (s , prf) n eq m le with NP.≤⇒≤′ le
false-extends-up (s , prf) n eq .n le | ≤′-refl = eq
false-extends-up (s , prf) n eq .(suc _) le | ≤′-step le' =
  false-extends-up-one (s , prf) _ (false-extends-up (s , prf) n eq _ (NP.≤′⇒≤ le'))

true-extends-down-one : (i : ℕ∞)(n : ℕ) → proj₁ i (suc n) ≡ true → proj₁ i n ≡ true
true-extends-down-one (s , prf) n eq with prf n | bool-split (s n)
true-extends-down-one (s , prf) n eq | p | inj₁ q rewrite eq | q = ⊥-elim (p tt)
true-extends-down-one (s , prf) n eq | p | inj₂ q = q

true-extends-down : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ true
                 → (m : ℕ) → m N.≤ n → proj₁ i m ≡ true
true-extends-down (s , prf) n eq m le with NP.≤⇒≤′ le
true-extends-down (s , prf) n eq .n le | ≤′-refl = eq
true-extends-down (s , prf) .(suc _) eq m le | ≤′-step le' =
  true-extends-down (s , prf) _ (true-extends-down-one (s , prf) _ eq) m (NP.≤′⇒≤ le')

¬nat→inf : (i : ℕ∞) → ((n : ℕ) → nat n ≢ i) → i ≡ inf
¬nat→inf i nn = Σ-ext (fext _ _ λ n → bool-flip (prf n)) (evidence-triv _ _ _)
  where extend-zeros : (n : ℕ)
                     → ((m : ℕ) → suc n N.≤ m → proj₁ i m ≡ false)
                     → proj₁ i n ≡ false
                     → ((m : ℕ) → n N.≤ m → proj₁ i m ≡ false)
        extend-zeros n prf eq m le with compare n m
        extend-zeros n prf eq .(suc (n + k)) le | less .n k = prf (suc (n + k)) (s≤s (m≤m+n _ _))
        extend-zeros n prf eq .n le | equal .n = eq
        extend-zeros .(suc (m + k)) prf eq m le | greater .m k = ⊥-elim (1+n≰n (≤-trans (s≤s (m≤m+n _ _)) le))

        behaves-as-n : (n : ℕ)
                     → ((m : ℕ) → m N.≤ n → proj₁ i m ≡ true)
                     → ((m : ℕ) → suc n N.≤ m → proj₁ i m ≡ false)
                     → (m : ℕ) → proj₁ (nat (suc n)) m ≡ proj₁ i m
        behaves-as-n n below above m with compare (suc n) m
        behaves-as-n n below above .(suc (suc n + k)) | less .(suc n) k with suc (suc (n + k)) NP.<? suc n
        ... | yes (s≤s p) = ⊥-elim (1+n≰n (≤-trans (s≤s (≤-trans (n≤1+n _) (s≤s (m≤m+n _ _)))) p))
        ... | no ¬p = sym (above (suc (suc (n + k))) (s≤s (≤-trans (n≤1+n _) (s≤s (m≤m+n _ _)))))
        behaves-as-n n below above .(suc n) | equal .(suc n) with suc n NP.<? suc n
        behaves-as-n n below above .(suc n) | equal .(suc n) | yes p = ⊥-elim (1+n≰n p)
        behaves-as-n n below above .(suc n) | equal .(suc n) | no ¬p = sym (above (suc n) ≤-refl)
        behaves-as-n .(m + k) below above m | greater .m k with m NP.<? suc (m + k)
        ... | yes p = sym (below m (m≤m+n _ _))
        ... | no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))

        contra : (n : ℕ) → ((m : ℕ) → n N.≤ m → proj₁ i m ≡ false) → ⊥
        contra zero prf = nn zero (ℕ∞-eq _ _ (fext _ _ λ n → sym (prf n z≤n)))
        contra (suc n) prf with proj₁ i n B.≟ false
        contra (suc n) prf | yes p = contra n (extend-zeros n prf p)
        contra (suc n) prf | no ¬p =
          nn (suc n) (ℕ∞-eq _ _ (fext _ _ λ x →
            behaves-as-n n ((true-extends-down i n (bool-flip ¬p))) ((false-extends-up i (suc n) (prf _ ≤-refl))) x))

        prf : (n : ℕ) → proj₁ i n ≡ false → ⊥
        prf n eq = contra n (false-extends-up i n eq)

extends : (ℕ → Set) → (ℕ∞ → Set) → Set
extends seq₁ seq₂ = (i : ℕ) → seq₁ i ≅ seq₂ (nat i)

extend-to-⊤ : (seq : ℕ → Set) → Σ (ℕ∞ → Set) λ s → extends seq s × s inf ≅ ⊤
extend-to-⊤ seq =  seq' , ext , (l , r , (lr , rl))
  where seq' = λ i → ∀ n → nat n ≡ i → seq n

        ext : extends seq seq'
        ext i = l , r , lr , rl
          where l : seq i → seq' (nat i)
                l xᵢ n eq with n N.≟ i
                l xᵢ n eq | yes p rewrite p = xᵢ
                l xᵢ n eq | no ¬p = ⊥-elim (¬p (nat-inj _ _ eq))

                r : seq' (nat i) → seq i
                r f = f i refl

                lr-cont : (a : seq' (nat i))(n : ℕ)(eq : nat n ≡ nat i) → (l ∘ r) a n eq ≡ id a n eq
                lr-cont a n eq with n N.≟ i
                ... | yes p rewrite p with eq
                lr-cont a n eq | yes p | refl = refl
                lr-cont a n eq | no ¬p = ⊥-elim (¬p (nat-inj _ _ eq))

                lr : l ∘ r ≡ id
                lr = fext _ _ λ a → fext _ _ λ n → fext _ _ λ eq -> lr-cont a n eq

                rl-cont : (a : seq i) → (r ∘ l) a ≡ id a
                rl-cont a with i N.≟ i
                rl-cont a | yes refl = refl
                rl-cont a | no ¬p = ⊥-elim (¬p refl)

                rl : r ∘ l ≡ id
                rl = fext _ _ λ s → rl-cont s

        l : ((n : ℕ) → nat n ≡ inf → seq n) → ⊤
        l _ = tt
        r : ⊤ → ((n : ℕ) → nat n ≡ inf → seq n)
        r _ n eq = ⊥-elim (inf-not-nat n eq)

        lr : l ∘ r ≡ id
        lr = fext (l ∘ r) id λ _ → refl
        rl : r ∘ l ≡ id
        rl = fext (r ∘ l) id λ a → fext (r tt) a λ n → fext (r tt n) (a n) λ eq → ⊥-elim (inf-not-nat n eq)

constant : Set → Set → (ℕ∞ → Set) → Set
constant A B seq = ((i : ℕ) → seq (nat i) ≅ A) × (seq inf ≅ B)

all-zeros : ℕ∞ → Set
all-zeros = proj₁ (extend-to-⊤ λ i → ⊥)

all-zeros-prop : constant ⊥ ⊤ all-zeros
all-zeros-prop = (λ i → ≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))
               , proj₂ (proj₂ (extend-to-⊤ λ i → ⊥))

mul : Set → (ℕ∞ → Set) → (ℕ∞ → Set)
mul A seq i = (seq i) × A

mul-prop : {A B : Set}{seq : ℕ∞ → Set}{i : ℕ∞} → seq i ≅ B → mul A seq i ≅ (B × A)
mul-prop (f , g , eq1 , eq2) =
  (λ p → (f (proj₁ p) , proj₂ p)) , (λ p → (g (proj₁ p), proj₂ p)) ,
  (fext _ _ λ p → ×-ext (cong-app eq1 (proj₁ p)) refl) ,
  (fext _ _ λ p → ×-ext (cong-app eq2 (proj₁ p)) refl)

⊥-converge-anywhere : (A : Set) → constant ⊥ A (mul A all-zeros)
⊥-converge-anywhere A =
  (λ i → ≅-trans (mul-prop {seq = all-zeros} (≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))) ⊥×-≅),
  (≅-trans (mul-prop {seq = all-zeros} (proj₂ (proj₂ (extend-to-⊤ λ i → ⊥)))) ⊤×-≅)

pow : Set → (ℕ∞ → Set) → (ℕ∞ → Set)
pow A seq i = seq i → A

pow-prop : {A B : Set}{seq : ℕ∞ → Set}{i : ℕ∞} → seq i ≅ B → pow A seq i ≅ (B → A)
pow-prop (f , g , eq1 , eq2) =
  (λ p b → p (g b)) , (λ p z → p (f z)) ,
  (fext _ _ λ x → fext _ _ λ b → cong x (cong-app eq1 b)) ,
  (fext _ _ λ x → fext _ _ λ a → cong x (cong-app eq2 a))

all-ones : ℕ∞ → Set
all-ones = proj₁ (extend-to-⊤ λ i → ⊤)

⊤-converges-⊥ : constant ⊤ ⊥ (pow ⊥ all-zeros)
⊤-converges-⊥ =
   (λ i → ≅-trans (pow-prop {seq = all-zeros} (≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))) ⊥⊥→-≅) ,
   ≅-trans (pow-prop {seq = all-zeros} (proj₂ (proj₂ (extend-to-⊤ λ i → ⊥)))) ⊥⊤→-≅

mul-pw : (ℕ∞ → Set) → (ℕ∞ → Set) → (ℕ∞ → Set)
mul-pw seq1 seq2 i = seq1 i × seq2 i

mul-pw-prop : {A B : Set}{seq1 seq2 : ℕ∞ → Set}{i : ℕ∞}
            → seq1 i ≅ A → seq2 i ≅ B → mul-pw seq1 seq2 i ≅ (A × B)
mul-pw-prop (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
  (λ p → (f1 (proj₁ p) , f2 (proj₂ p))) , (λ p → (g1 (proj₁ p), g2 (proj₂ p))) ,
  (fext _ _ λ p → ×-ext (cong-app eq11 (proj₁ p)) (cong-app eq21 (proj₂ p))) ,
  (fext _ _ λ p → ×-ext (cong-app eq12 (proj₁ p)) (cong-app eq22 (proj₂ p)))

converges-as : (ℕ∞ → Set) → Set → (ℕ∞ → Set) → Set
converges-as ref A s = ((i : ℕ) → ref (nat i) ≅ s (nat i)) × s inf ≅ A

all-converges-⊥ : (t : ℕ∞ → Set) → Σ (ℕ∞ → Set) λ s → converges-as t ⊥ s
all-converges-⊥ t =
  mul-pw (pow ⊥ all-zeros) t ,
  (λ i → ≅-trans (≅-sym ⊤×-≅) (≅-sym (mul-pw-prop {seq1 = pow ⊥ all-zeros} {seq2 = t} (proj₁ ⊤-converges-⊥ i) ≅-refl))) ,
  ≅-trans (mul-pw-prop {seq1 = pow ⊥ all-zeros} {seq2 = t} (proj₂ ⊤-converges-⊥) ≅-refl) ⊥×-≅

sum-pw : (ℕ∞ → Set) → (ℕ∞ → Set) → (ℕ∞ → Set)
sum-pw seq1 seq2 i = seq1 i ⊎ seq2 i

sum-pw-prop : {A B : Set}{seq1 seq2 : ℕ∞ → Set}{i : ℕ∞}
            → seq1 i ≅ A → seq2 i ≅ B → sum-pw seq1 seq2 i ≅ (A ⊎ B)
sum-pw-prop (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
  S.map f1 f2 , S.map g1 g2 ,
  (fext _ _
    (⊎-ext {f = (S.map f1 f2 ∘ S.map g1 g2)} {g = id}
      (λ a → cong inj₁ (cong-app eq11 a))
      (λ b → cong inj₂ (cong-app eq21 b)))) ,
  fext _ _
    (⊎-ext {f = (S.map g1 g2 ∘ S.map f1 f2)} {g = id}
      (λ a → cong inj₁ (cong-app eq12 a))
      (λ a → cong inj₂ (cong-app eq22 a)))

all-converge-all : (t : ℕ∞ → Set)(A : Set) → Σ (ℕ∞ → Set) λ s → converges-as t A s
all-converge-all t A =
  sum-pw (mul A all-zeros) (proj₁ (all-converges-⊥ t)) ,
  (λ i →
    ≅-trans (≅-sym ⊥⊎-≅)
      (≅-sym (sum-pw-prop {seq1 = (mul A all-zeros)} {seq2 = proj₁ (all-converges-⊥ t)}
        (proj₁ (⊥-converge-anywhere A) i)
        (≅-sym (proj₁ (proj₂ (all-converges-⊥ t)) i))))) ,
  (≅-trans
    (sum-pw-prop {seq1 = (mul A all-zeros)} {seq2 = proj₁ (all-converges-⊥ t)}
      (proj₂ (⊥-converge-anywhere A))
      (proj₂ (proj₂ (all-converges-⊥ t))))
    ⊎⊥-≅)

wlpo : Set
wlpo = (f : ℕ∞) → (f ≡ inf) ⊎ (f ≢ inf)

extensional : (Set → Bool) → Set₁
extensional f = (A B : Set) → A ≅ B → f A ≡ f B

nontrivial-map : (Set → Bool) → Set₁
nontrivial-map f = extensional f × Σ Set λ A → Σ Set λ B → (f A ≡ true) × (f B ≡ false)

nontrivial-implies-wlpo : Σ (Set → Bool) nontrivial-map → wlpo
nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i with all-converge-all (λ i → A) B
... | s , fin-case , inf-case with f (s i) B.≟ true
nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i | s , fin-case , inf-case | no ¬p =
  inj₁ (¬nat→inf i λ n eq → contra (bool-flip ¬p) (subst (λ x → s x ≅ A) eq (≅-sym (fin-case n))))
  where contra : f (s i) ≡ false → s i ≅ A → ⊥
        contra eq c with ext _ _ c
        contra eq c | p rewrite eq | eq1 = true≢false (sym p)
nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i | s , fin-case , inf-case | yes p =
  inj₂ λ eq → contra p (subst (λ x → s x ≅ B) (sym eq) inf-case)
  where contra : f (s i) ≡ true → s i ≅ B → ⊥
        contra eq c with ext _ _ c
        contra eq c | p rewrite eq | eq2 = true≢false p
	module intrinsic where
	open import Function using (_∘_; id)
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Data.Empty
	open import Data.Unit
	open import Data.Product
	open import Data.Sum as S
	open import Data.Bool as B
	open import Data.Nat as N
	open import Data.Nat.Properties as NP

	postulate fext : {A : Set}{B : A → Set}(f g : (a : A) → B a) → ((a : A) → f a ≡ g a) → f ≡ g

	fold : {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
	fold f g (inj₁ x) = f x
	fold f g (inj₂ y) = g y

	Σ-ext : {A : Set}{B : A → Set}{p q : Σ A B}(eq : proj₁ p ≡ proj₁ q) → subst B eq (proj₂ p) ≡ proj₂ q → p ≡ q
	Σ-ext refl refl = refl

	×-ext : {A B : Set}{p q : A × B} → proj₁ p ≡ proj₁ q → proj₂ p ≡ proj₂ q → p ≡ q
	×-ext refl refl = refl

	⊎-ext : {A B C : Set}{f g : A ⊎ B → C}
	→ ((a : A) → f (inj₁ a) ≡ g (inj₁ a))
	→ ((b : B) → f (inj₂ b) ≡ g (inj₂ b))
	→ (s : A ⊎ B) → f s ≡ g s
	⊎-ext l r (inj₁ x) = l x
	⊎-ext l r (inj₂ y) = r y

	bool-split : (b : Bool) → (b ≡ false) ⊎ (b ≡ true)
	bool-split true = inj₂ refl
	bool-split false = inj₁ refl

	true≢false : true ≢ false
	true≢false ()

	bool-flip : {b1 b2 : Bool} → b1 ≢ b2 → b1 ≡ not b2
	bool-flip {false} {false} eq = ⊥-elim (eq refl)
	bool-flip {false} {true} eq = refl
	bool-flip {true} {false} eq = refl
	bool-flip {true} {true} eq = ⊥-elim (eq refl)

	_≅_ : Set → Set → Set
	A ≅ B = Σ (A → B) λ f → Σ (B → A) λ g → f ∘ g ≡ id × g ∘ f ≡ id

	≅-refl : {A : Set} → A ≅ A
	≅-refl = id , id , refl , refl

	≅-sym : {A B : Set} → A ≅ B → B ≅ A
	≅-sym (f , g , eq1 , eq2) = (g , f , eq2 , eq1)

	≅-trans : {A B C : Set} → A ≅ B → B ≅ C → A ≅ C
	≅-trans {A} {B} {C} (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
	(λ z → f2 (f1 z)) , (λ z → g1 (g2 z)) ,
	(fext _ _ eq1) , fext _ _ eq2
	where eq1 : (c : C) → f2 (f1 (g1 (g2 c))) ≡ c
	eq1 c rewrite cong-app eq11 (g2 c) \| cong-app eq21 c = refl
	eq2 : (a : A) → g1 (g2 (f2 (f1 a))) ≡ a
	eq2 a rewrite cong-app eq22 (f1 a) \| cong-app eq12 a = refl

	⊥×-≅ : {A : Set} → (⊥ × A) ≅ ⊥
	⊥×-≅ = proj₁ , (λ ()) , fext _ _ (λ ()) , fext _ _ λ p → ⊥-elim (proj₁ p)

	⊤×-≅ : {A : Set} → (⊤ × A) ≅ A
	⊤×-≅ = proj₂ , (λ a → tt , a) , refl , fext _ _ λ p → ×-ext refl refl

	⊥⊤→-≅ : (⊤ → ⊥) ≅ ⊥
	⊥⊤→-≅ = (λ z → z tt) , (λ z _ → z) , refl , fext _ _ λ a → ⊥-elim (a tt)

	⊥⊥→-≅ : (⊥ → ⊥) ≅ ⊤
	⊥⊥→-≅ = (λ _ → tt) , (λ _ z → z) , (fext _ _ λ x → refl) , fext _ _ λ x → fext _ _ λ ()

	⊥⊎-≅ : {A : Set} → (⊥ ⊎ A) ≅ A
	⊥⊎-≅ = fold ⊥-elim id , inj₂ , (fext _ _ λ a → refl) , fext _ _ (⊎-ext (λ ()) (λ b → refl))

	⊎⊥-≅ : {A : Set} → (A ⊎ ⊥) ≅ A
	⊎⊥-≅ = fold id ⊥-elim , inj₁ , (fext _ _ λ a → refl) , fext _ _ (⊎-ext (λ b → refl) (λ ()))

	coerce : Bool → Set
	coerce false = ⊤
	coerce true = ⊥

	ℕ∞ : Set
	ℕ∞ = Σ (ℕ → Bool) λ f → (i : ℕ) → coerce (f i) → coerce (f (suc i))

	evidence-triv : (f : ℕ → Bool)(a b : (i : ℕ) → coerce (f i) → coerce (f (suc i)))
	→ a ≡ b
	evidence-triv f a b = fext _ _ λ i → prf f i (a i) (b i)
	where prf : (f : ℕ → Bool)(i : ℕ)(a b : coerce (f i) → coerce (f (suc i))) → a ≡ b
	prf f i a b with f (suc i) \| f i
	prf f i a b \| p \| true = fext _ _ λ ()
	prf f i a b \| true \| false = ⊥-elim (b tt)
	prf f i a b \| false \| false = fext _ _ λ _ → refl

	ℕ∞-eq : (i j : ℕ∞) → proj₁ i ≡ proj₁ j → i ≡ j
	ℕ∞-eq i j eq = Σ-ext eq (evidence-triv _ _ _)

	raw-nat : ℕ → ℕ → Bool
	raw-nat upper n with n NP.<? upper
	... \| yes _ = true
	... \| no _ = false

	nat : ℕ → ℕ∞
	nat n = raw-nat n , prf n
	where prf : (n : ℕ)(i : ℕ) → coerce (raw-nat n i) → coerce (raw-nat n (suc i))
	prf n i p with i NP.<? n
	prf n i () \| yes p₁
	prf n i p \| no ¬p with suc i NP.<? n
	prf n i p \| no ¬p \| yes q = ¬p (≤-trans (n≤1+n (suc i)) q)
	prf n i p \| no ¬p \| no _ = tt

	raw-nat-inj : (n m : ℕ) → raw-nat n ≡ raw-nat m → n ≡ m
	raw-nat-inj n m eq with N.compare n m
	raw-nat-inj n .(suc (n + k)) eq \| less .n k with cong-app eq n
	... \| eq' with n NP.<? n \| n NP.<? suc (n + k)
	... \| yes p \| _ = ⊥-elim (1+n≰n p)
	raw-nat-inj n .(suc (n + k)) eq \| less .n k \| () \| no ¬p \| yes p
	... \| no _ \| no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))
	raw-nat-inj n .n eq \| equal .n = refl
	raw-nat-inj .(suc (m + k)) m eq \| greater .m k with cong-app eq m
	... \| eq' with m NP.<? m \| m NP.<? suc (m + k)
	... \| yes p \| _ = ⊥-elim (1+n≰n p)
	raw-nat-inj .(suc (m + k)) m eq \| greater .m k \| () \| no ¬p \| yes p
	... \| no _ \| no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))

	nat-inj : (n m : ℕ) → nat n ≡ nat m → n ≡ m
	nat-inj n m eq = raw-nat-inj n m (cong proj₁ eq)

	inf : ℕ∞
	inf = (λ _ → true), (λ i ())

	inf-not-nat : (n : ℕ) → nat n ≢ inf
	inf-not-nat n eq with cong-app (cong proj₁ eq) (suc n)
	inf-not-nat n eq \| p with suc n NP.<? n
	inf-not-nat n eq \| p \| yes p₁ = ⊥-elim (1+n≰n (≤-trans (n≤1+n (suc n)) p₁))
	inf-not-nat n eq \| () \| no ¬p

	false-extends-up-one : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ false → proj₁ i (suc n) ≡ false
	false-extends-up-one (s , prf) n eq with prf n \| bool-split (s (suc n))
	false-extends-up-one (s , prf) n eq \| p \| inj₁ q = q
	false-extends-up-one (s , prf) n eq \| p \| inj₂ q rewrite eq \| q = ⊥-elim (p tt)

	false-extends-up : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ false
	→ (m : ℕ) → n N.≤ m → proj₁ i m ≡ false
	false-extends-up (s , prf) n eq m le with NP.≤⇒≤′ le
	false-extends-up (s , prf) n eq .n le \| ≤′-refl = eq
	false-extends-up (s , prf) n eq .(suc _) le \| ≤′-step le' =
	false-extends-up-one (s , prf) _ (false-extends-up (s , prf) n eq _ (NP.≤′⇒≤ le'))

	true-extends-down-one : (i : ℕ∞)(n : ℕ) → proj₁ i (suc n) ≡ true → proj₁ i n ≡ true
	true-extends-down-one (s , prf) n eq with prf n \| bool-split (s n)
	true-extends-down-one (s , prf) n eq \| p \| inj₁ q rewrite eq \| q = ⊥-elim (p tt)
	true-extends-down-one (s , prf) n eq \| p \| inj₂ q = q

	true-extends-down : (i : ℕ∞)(n : ℕ) → proj₁ i n ≡ true
	→ (m : ℕ) → m N.≤ n → proj₁ i m ≡ true
	true-extends-down (s , prf) n eq m le with NP.≤⇒≤′ le
	true-extends-down (s , prf) n eq .n le \| ≤′-refl = eq
	true-extends-down (s , prf) .(suc _) eq m le \| ≤′-step le' =
	true-extends-down (s , prf) _ (true-extends-down-one (s , prf) _ eq) m (NP.≤′⇒≤ le')

	¬nat→inf : (i : ℕ∞) → ((n : ℕ) → nat n ≢ i) → i ≡ inf
	¬nat→inf i nn = Σ-ext (fext _ _ λ n → bool-flip (prf n)) (evidence-triv _ _ _)
	where extend-zeros : (n : ℕ)
	→ ((m : ℕ) → suc n N.≤ m → proj₁ i m ≡ false)
	→ proj₁ i n ≡ false
	→ ((m : ℕ) → n N.≤ m → proj₁ i m ≡ false)
	extend-zeros n prf eq m le with compare n m
	extend-zeros n prf eq .(suc (n + k)) le \| less .n k = prf (suc (n + k)) (s≤s (m≤m+n _ _))
	extend-zeros n prf eq .n le \| equal .n = eq
	extend-zeros .(suc (m + k)) prf eq m le \| greater .m k = ⊥-elim (1+n≰n (≤-trans (s≤s (m≤m+n _ _)) le))

	behaves-as-n : (n : ℕ)
	→ ((m : ℕ) → m N.≤ n → proj₁ i m ≡ true)
	→ ((m : ℕ) → suc n N.≤ m → proj₁ i m ≡ false)
	→ (m : ℕ) → proj₁ (nat (suc n)) m ≡ proj₁ i m
	behaves-as-n n below above m with compare (suc n) m
	behaves-as-n n below above .(suc (suc n + k)) \| less .(suc n) k with suc (suc (n + k)) NP.<? suc n
	... \| yes (s≤s p) = ⊥-elim (1+n≰n (≤-trans (s≤s (≤-trans (n≤1+n _) (s≤s (m≤m+n _ _)))) p))
	... \| no ¬p = sym (above (suc (suc (n + k))) (s≤s (≤-trans (n≤1+n _) (s≤s (m≤m+n _ _)))))
	behaves-as-n n below above .(suc n) \| equal .(suc n) with suc n NP.<? suc n
	behaves-as-n n below above .(suc n) \| equal .(suc n) \| yes p = ⊥-elim (1+n≰n p)
	behaves-as-n n below above .(suc n) \| equal .(suc n) \| no ¬p = sym (above (suc n) ≤-refl)
	behaves-as-n .(m + k) below above m \| greater .m k with m NP.<? suc (m + k)
	... \| yes p = sym (below m (m≤m+n _ _))
	... \| no ¬p = ⊥-elim (¬p (s≤s (m≤m+n _ _)))

	contra : (n : ℕ) → ((m : ℕ) → n N.≤ m → proj₁ i m ≡ false) → ⊥
	contra zero prf = nn zero (ℕ∞-eq _ _ (fext _ _ λ n → sym (prf n z≤n)))
	contra (suc n) prf with proj₁ i n B.≟ false
	contra (suc n) prf \| yes p = contra n (extend-zeros n prf p)
	contra (suc n) prf \| no ¬p =
	nn (suc n) (ℕ∞-eq _ _ (fext _ _ λ x →
	behaves-as-n n ((true-extends-down i n (bool-flip ¬p))) ((false-extends-up i (suc n) (prf _ ≤-refl))) x))

	prf : (n : ℕ) → proj₁ i n ≡ false → ⊥
	prf n eq = contra n (false-extends-up i n eq)

	extends : (ℕ → Set) → (ℕ∞ → Set) → Set
	extends seq₁ seq₂ = (i : ℕ) → seq₁ i ≅ seq₂ (nat i)

	extend-to-⊤ : (seq : ℕ → Set) → Σ (ℕ∞ → Set) λ s → extends seq s × s inf ≅ ⊤
	extend-to-⊤ seq = seq' , ext , (l , r , (lr , rl))
	where seq' = λ i → ∀ n → nat n ≡ i → seq n

	ext : extends seq seq'
	ext i = l , r , lr , rl
	where l : seq i → seq' (nat i)
	l xᵢ n eq with n N.≟ i
	l xᵢ n eq \| yes p rewrite p = xᵢ
	l xᵢ n eq \| no ¬p = ⊥-elim (¬p (nat-inj _ _ eq))

	r : seq' (nat i) → seq i
	r f = f i refl

	lr-cont : (a : seq' (nat i))(n : ℕ)(eq : nat n ≡ nat i) → (l ∘ r) a n eq ≡ id a n eq
	lr-cont a n eq with n N.≟ i
	... \| yes p rewrite p with eq
	lr-cont a n eq \| yes p \| refl = refl
	lr-cont a n eq \| no ¬p = ⊥-elim (¬p (nat-inj _ _ eq))

	lr : l ∘ r ≡ id
	lr = fext _ _ λ a → fext _ _ λ n → fext _ _ λ eq -> lr-cont a n eq

	rl-cont : (a : seq i) → (r ∘ l) a ≡ id a
	rl-cont a with i N.≟ i
	rl-cont a \| yes refl = refl
	rl-cont a \| no ¬p = ⊥-elim (¬p refl)

	rl : r ∘ l ≡ id
	rl = fext _ _ λ s → rl-cont s

	l : ((n : ℕ) → nat n ≡ inf → seq n) → ⊤
	l _ = tt
	r : ⊤ → ((n : ℕ) → nat n ≡ inf → seq n)
	r _ n eq = ⊥-elim (inf-not-nat n eq)

	lr : l ∘ r ≡ id
	lr = fext (l ∘ r) id λ _ → refl
	rl : r ∘ l ≡ id
	rl = fext (r ∘ l) id λ a → fext (r tt) a λ n → fext (r tt n) (a n) λ eq → ⊥-elim (inf-not-nat n eq)

	constant : Set → Set → (ℕ∞ → Set) → Set
	constant A B seq = ((i : ℕ) → seq (nat i) ≅ A) × (seq inf ≅ B)

	all-zeros : ℕ∞ → Set
	all-zeros = proj₁ (extend-to-⊤ λ i → ⊥)

	all-zeros-prop : constant ⊥ ⊤ all-zeros
	all-zeros-prop = (λ i → ≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))
	, proj₂ (proj₂ (extend-to-⊤ λ i → ⊥))

	mul : Set → (ℕ∞ → Set) → (ℕ∞ → Set)
	mul A seq i = (seq i) × A

	mul-prop : {A B : Set}{seq : ℕ∞ → Set}{i : ℕ∞} → seq i ≅ B → mul A seq i ≅ (B × A)
	mul-prop (f , g , eq1 , eq2) =
	(λ p → (f (proj₁ p) , proj₂ p)) , (λ p → (g (proj₁ p), proj₂ p)) ,
	(fext _ _ λ p → ×-ext (cong-app eq1 (proj₁ p)) refl) ,
	(fext _ _ λ p → ×-ext (cong-app eq2 (proj₁ p)) refl)

	⊥-converge-anywhere : (A : Set) → constant ⊥ A (mul A all-zeros)
	⊥-converge-anywhere A =
	(λ i → ≅-trans (mul-prop {seq = all-zeros} (≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))) ⊥×-≅),
	(≅-trans (mul-prop {seq = all-zeros} (proj₂ (proj₂ (extend-to-⊤ λ i → ⊥)))) ⊤×-≅)

	pow : Set → (ℕ∞ → Set) → (ℕ∞ → Set)
	pow A seq i = seq i → A

	pow-prop : {A B : Set}{seq : ℕ∞ → Set}{i : ℕ∞} → seq i ≅ B → pow A seq i ≅ (B → A)
	pow-prop (f , g , eq1 , eq2) =
	(λ p b → p (g b)) , (λ p z → p (f z)) ,
	(fext _ _ λ x → fext _ _ λ b → cong x (cong-app eq1 b)) ,
	(fext _ _ λ x → fext _ _ λ a → cong x (cong-app eq2 a))

	all-ones : ℕ∞ → Set
	all-ones = proj₁ (extend-to-⊤ λ i → ⊤)

	⊤-converges-⊥ : constant ⊤ ⊥ (pow ⊥ all-zeros)
	⊤-converges-⊥ =
	(λ i → ≅-trans (pow-prop {seq = all-zeros} (≅-sym (proj₁ (proj₂ (extend-to-⊤ λ i → ⊥)) i))) ⊥⊥→-≅) ,
	≅-trans (pow-prop {seq = all-zeros} (proj₂ (proj₂ (extend-to-⊤ λ i → ⊥)))) ⊥⊤→-≅

	mul-pw : (ℕ∞ → Set) → (ℕ∞ → Set) → (ℕ∞ → Set)
	mul-pw seq1 seq2 i = seq1 i × seq2 i

	mul-pw-prop : {A B : Set}{seq1 seq2 : ℕ∞ → Set}{i : ℕ∞}
	→ seq1 i ≅ A → seq2 i ≅ B → mul-pw seq1 seq2 i ≅ (A × B)
	mul-pw-prop (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
	(λ p → (f1 (proj₁ p) , f2 (proj₂ p))) , (λ p → (g1 (proj₁ p), g2 (proj₂ p))) ,
	(fext _ _ λ p → ×-ext (cong-app eq11 (proj₁ p)) (cong-app eq21 (proj₂ p))) ,
	(fext _ _ λ p → ×-ext (cong-app eq12 (proj₁ p)) (cong-app eq22 (proj₂ p)))

	converges-as : (ℕ∞ → Set) → Set → (ℕ∞ → Set) → Set
	converges-as ref A s = ((i : ℕ) → ref (nat i) ≅ s (nat i)) × s inf ≅ A

	all-converges-⊥ : (t : ℕ∞ → Set) → Σ (ℕ∞ → Set) λ s → converges-as t ⊥ s
	all-converges-⊥ t =
	mul-pw (pow ⊥ all-zeros) t ,
	(λ i → ≅-trans (≅-sym ⊤×-≅) (≅-sym (mul-pw-prop {seq1 = pow ⊥ all-zeros} {seq2 = t} (proj₁ ⊤-converges-⊥ i) ≅-refl))) ,
	≅-trans (mul-pw-prop {seq1 = pow ⊥ all-zeros} {seq2 = t} (proj₂ ⊤-converges-⊥) ≅-refl) ⊥×-≅

	sum-pw : (ℕ∞ → Set) → (ℕ∞ → Set) → (ℕ∞ → Set)
	sum-pw seq1 seq2 i = seq1 i ⊎ seq2 i

	sum-pw-prop : {A B : Set}{seq1 seq2 : ℕ∞ → Set}{i : ℕ∞}
	→ seq1 i ≅ A → seq2 i ≅ B → sum-pw seq1 seq2 i ≅ (A ⊎ B)
	sum-pw-prop (f1 , g1 , eq11 , eq12) (f2 , g2 , eq21 , eq22) =
	S.map f1 f2 , S.map g1 g2 ,
	(fext _ _
	(⊎-ext {f = (S.map f1 f2 ∘ S.map g1 g2)} {g = id}
	(λ a → cong inj₁ (cong-app eq11 a))
	(λ b → cong inj₂ (cong-app eq21 b)))) ,
	fext _ _
	(⊎-ext {f = (S.map g1 g2 ∘ S.map f1 f2)} {g = id}
	(λ a → cong inj₁ (cong-app eq12 a))
	(λ a → cong inj₂ (cong-app eq22 a)))

	all-converge-all : (t : ℕ∞ → Set)(A : Set) → Σ (ℕ∞ → Set) λ s → converges-as t A s
	all-converge-all t A =
	sum-pw (mul A all-zeros) (proj₁ (all-converges-⊥ t)) ,
	(λ i →
	≅-trans (≅-sym ⊥⊎-≅)
	(≅-sym (sum-pw-prop {seq1 = (mul A all-zeros)} {seq2 = proj₁ (all-converges-⊥ t)}
	(proj₁ (⊥-converge-anywhere A) i)
	(≅-sym (proj₁ (proj₂ (all-converges-⊥ t)) i))))) ,
	(≅-trans
	(sum-pw-prop {seq1 = (mul A all-zeros)} {seq2 = proj₁ (all-converges-⊥ t)}
	(proj₂ (⊥-converge-anywhere A))
	(proj₂ (proj₂ (all-converges-⊥ t))))
	⊎⊥-≅)

	wlpo : Set
	wlpo = (f : ℕ∞) → (f ≡ inf) ⊎ (f ≢ inf)

	extensional : (Set → Bool) → Set₁
	extensional f = (A B : Set) → A ≅ B → f A ≡ f B

	nontrivial-map : (Set → Bool) → Set₁
	nontrivial-map f = extensional f × Σ Set λ A → Σ Set λ B → (f A ≡ true) × (f B ≡ false)

	nontrivial-implies-wlpo : Σ (Set → Bool) nontrivial-map → wlpo
	nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i with all-converge-all (λ i → A) B
	... \| s , fin-case , inf-case with f (s i) B.≟ true
	nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i \| s , fin-case , inf-case \| no ¬p =
	inj₁ (¬nat→inf i λ n eq → contra (bool-flip ¬p) (subst (λ x → s x ≅ A) eq (≅-sym (fin-case n))))
	where contra : f (s i) ≡ false → s i ≅ A → ⊥
	contra eq c with ext _ _ c
	contra eq c \| p rewrite eq \| eq1 = true≢false (sym p)
	nontrivial-implies-wlpo (f , ext , A , B , eq1 , eq2) i \| s , fin-case , inf-case \| yes p =
	inj₂ λ eq → contra p (subst (λ x → s x ≅ B) (sym eq) inf-case)
	where contra : f (s i) ≡ true → s i ≅ B → ⊥
	contra eq c with ext _ _ c
	contra eq c \| p rewrite eq \| eq2 = true≢false p