Dedekind.agda

{-# OPTIONS --cubical --safe #-}
module Dedekind where

open import Cubical.Foundations.Everything

open import Cubical.Data.Sigma
open import Cubical.Data.Nat as Nat
open import Cubical.Data.Bool as Bool

elimBool : ∀ {ℓ} {P : Bool → Type ℓ} (a0 : P true) (a1 : P false)
           → (x : Bool) → P x
elimBool a0 a1 true  = a0
elimBool a0 a1 false = a1

-- initial κ-frames

module Frame {ℓ} (κ : Type ℓ) where

  data Ω : Type ℓ
  data _→ʷ_ : Ω → Ω → Type ℓ
  pathToEquiv-Ω : ∀ {x y} → x ≡ y → (x →ʷ y) × (y →ʷ x)

  data Ω where
    ⊥ ⊤ : Ω
    _∩_ : Ω → Ω → Ω
    ∃ : (κ → Ω) → Ω
    ua-Ω : ∀ {x y} → (x →ʷ y) × (y →ʷ x) → x ≡ y
    uaη-Ω : ∀ {x y} (p : x ≡ y) → ua-Ω (pathToEquiv-Ω p) ≡ p

  data _→ʷ_ where
    ⊥-init : ∀ {x} → ⊥ →ʷ x
    ⊤-term : ∀ {x} → x →ʷ ⊤
    ∩-pr₁ : ∀ {x y} → x ∩ y →ʷ x
    ∩-pr₂ : ∀ {x y} → x ∩ y →ʷ y
    ∩-rec : ∀ {x y} {b} → (b →ʷ x) → (b →ʷ y) → b →ʷ x ∩ y
    ∃-inj : ∀ {P} n → P n →ʷ ∃ P
    ∃-rec : ∀ {P} {b} → (∀ n → P n →ʷ b) → ∃ P →ʷ b
    ∩-∃-distrib : ∀ {P} {x} → (∃ P) ∩ x →ʷ ∃ (λ n → (P n) ∩ x)
    _∘ʷ_ : ∀ {x y z} → y →ʷ z → x →ʷ y → x →ʷ z
    pathTo→ʷ : ∀ {x y} → x ≡ y → x →ʷ y
    →ʷ-isProp : ∀ {x y} → isProp (x →ʷ y)

  pathToEquiv-Ω p = (pathTo→ʷ p) , (pathTo→ʷ (sym p))

  univalence-Ω : ∀ {x y} → (x →ʷ y) × (y →ʷ x) ≃ (x ≡ y)
  univalence-Ω = isoToEquiv (iso ua-Ω pathToEquiv-Ω uaη-Ω
                                 (λ _ → isProp× →ʷ-isProp →ʷ-isProp _ _))

  isSetΩ : isSet Ω
  isSetΩ _ _ = subst isProp (ua univalence-Ω) (isProp× →ʷ-isProp →ʷ-isProp)

  infixl 2 _→ʷ_
  infixr 9 _∘ʷ_

  _→ʷ⟨_⟩_ : (x : Ω) {y z : Ω} → x →ʷ y → y →ʷ z → x →ʷ z
  _ →ʷ⟨ f ⟩ g = g ∘ʷ f

  infixr 2 _→ʷ⟨_⟩_

  _∎ʷ : (x : Ω) → x →ʷ x
  _ ∎ʷ = pathTo→ʷ refl

  -- some basic lemmas

  ∩-monoˡ : ∀ {x y z} → x →ʷ y → x ∩ z →ʷ y ∩ z
  ∩-monoˡ f = ∩-rec (f ∘ʷ ∩-pr₁) ∩-pr₂

  ∩-monoʳ : ∀ {x y z} → y →ʷ z → x ∩ y →ʷ x ∩ z
  ∩-monoʳ f = ∩-rec ∩-pr₁ (f ∘ʷ ∩-pr₂)

  ∩-comm : ∀ {x y} → x ∩ y →ʷ y ∩ x
  ∩-comm = ∩-rec ∩-pr₂ ∩-pr₁

  module Disjunction (sur : κ → Bool) where

    _∪_ : Ω → Ω → Ω
    x ∪ y = ∃ (caseBool x y ∘ sur)

    ∪-rec : ∀ {x y} {b} → (x →ʷ b) → (y →ʷ b) → x ∪ y →ʷ b
    ∪-rec f g = ∃-rec (elimBool {P = λ z → caseBool _ _ z →ʷ _} f g ∘ sur)

    ∩-∪-distrib : ∀ {x y z} → (x ∪ y) ∩ z →ʷ (x ∩ z) ∪ (y ∩ z)
    ∩-∪-distrib {x} {y} {z} =
      (∃ (caseBool x y ∘ sur)) ∩ z       →ʷ⟨ ∩-∃-distrib ⟩
      ∃ ((_∩ z) ∘ caseBool x y ∘ sur)    →ʷ⟨ pathTo→ʷ (cong (∃ ∘ (_∘ sur)) (lem (_∩ z))) ⟩
      ∃ (caseBool (x ∩ z) (y ∩ z) ∘ sur) ∎ʷ
      where lem : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x y : A}
                  → (f : A → B) → f ∘ caseBool x y ≡ caseBool (f x) (f y)
            lem f = funExt (elimBool refl refl)

-- Dedekind cuts

module Dedekind {ℓ} (A : Type ℓ) (e : A ≃ ℕ) (_<_ : A → A → Frame.Ω A) where
  open Frame A
  open Frame.Disjunction A (caseNat true false ∘ e .fst)

  record isCut (L R : A → Ω) : Type ℓ where
  
    field
      disj : ∀ a → L a ∩ R a →ʷ ⊥
      loc : ∀ a b → (a < b) →ʷ (L a) ∪ (R b)
  
    -- this is enough to show that L (resp. R) is closed downward (resp. upward)
  
    closedL : ∀ a → ∃ (λ b → (a < b) ∩ L b) →ʷ L a
    closedL a = ∃-rec (λ b →
      (a < b)     ∩ L b         →ʷ⟨ ∩-monoˡ (loc a b) ⟩
      (L a ∪ R b) ∩ L b         →ʷ⟨ ∩-∪-distrib ⟩
      (L a ∩ L b) ∪ (R b ∩ L b) →ʷ⟨ ∪-rec ∩-pr₁ (⊥-init ∘ʷ (disj b) ∘ʷ ∩-comm) ⟩
      L a                       ∎ʷ )
  
    closedR : ∀ b → ∃ (λ a → (a < b) ∩ R a) →ʷ R b
    closedR b = ∃-rec (λ a →
      (a < b)     ∩ R a         →ʷ⟨ ∩-monoˡ (loc a b) ⟩
      (L a ∪ R b) ∩ R a         →ʷ⟨ ∩-∪-distrib ⟩
      (L a ∩ R a) ∪ (R b ∩ R a) →ʷ⟨ ∪-rec (⊥-init ∘ʷ (disj a)) ∩-pr₁ ⟩
      R b                       ∎ʷ )
  
    -- we also require the converse, that L (resp. R) is open upward (resp. downward)

    field
      openL : ∀ a → L a →ʷ ∃ (λ b → (a < b) ∩ L b)
      openR : ∀ b → R b →ʷ ∃ (λ a → (a < b) ∩ R a)
  
    field
      inhabL : ⊤ →ʷ ∃ (λ a → L a)
      inhabR : ⊤ →ʷ ∃ (λ b → R b)

  open isCut public

  isPropIsCut : ∀ L R → isProp (isCut L R)
  isPropIsCut L R = {!!}

  Cuts : Type ℓ
  Cuts = Σ[ L ∈ (A → Ω) ] Σ[ R ∈ (A → Ω) ] isCut L R

  isSetCuts : isSet Cuts
  isSetCuts = isSetΣ (isSetΠ (λ _ → isSetΩ)) (λ L →
               isSetΣ (isSetΠ (λ _ → isSetΩ)) (λ R →
                isProp→isSet (isPropIsCut L R)))