A proof that choice implies excluded middle in cubical Agda

Diaconescu.agda

{-# OPTIONS --cubical #-}
module Diaconescu where

  open import Data.Bool using (true; false)
  open import Data.Empty
  open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂)
  open import Data.Unit
  open import Level renaming (zero to lzero; suc to lsuc)
  open import Relation.Binary.PropositionalEquality as ≡p
    using (inspect)
    renaming (_≡_ to _≡p_)
  open import Relation.Nullary.Reflects using (invert)
  open import Relation.Nullary
  open import Relation.Nullary.Decidable

  open import Cubical.Foundations.Everything
    using ( Type; _≡_; refl; _⁻¹; I; i0; i1; PathP; Path; isProp→PathP
          ; isoToPath; toPathP; transp; _∧_; _∨_; ~_; subst; cong; _∙_
          ; _∘_; funExt
          )
    renaming ( isProp to IsProp; isPropIsProp to IsProp-IsProp
             ; isContr to IsContr; isSet to IsSet
             )
  open import Cubical.HITs.PropositionalTruncation

  record HProp (ℓ : Level) : Set (lsuc ℓ) where
    field
      type : Type ℓ
      isProp : IsProp type
  open HProp public

  record HSet (ℓ : Level) : Set (lsuc ℓ) where
    field
      type : Type ℓ
      isSet : IsSet type
  open HSet public

  IsSurjection : ∀ {a b} {A : Type a} {B : Type b} (f : A → B) → Type (a ⊔ b)
  IsSurjection {A = A} {B} f = (b : B) → ∥ Σ[ a ∈ A ] f a ≡ b ∥

  record Surjection {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
    field
      act : A → B
      isSurjection : IsSurjection act

  IsStrongSurjection : ∀ {a b} {A : Type a} {B : Type b}
                       (f : A → B) → Type (a ⊔ b)
  IsStrongSurjection {A = A} {B} f = (b : B) → Σ[ a ∈ A ] f a ≡ b

  IsSplitSurjection : ∀ {a b} {A : Type a} {B : Type b}
                      (f : A → B) → Type (a ⊔ b)
  IsSplitSurjection f = ∥ IsStrongSurjection f ∥

  Section : ∀ {a b} {A : Type a} {B : Type b} (f : A → B) → Type (a ⊔ b)
  Section {A = A} {B} f = Σ[ r ∈ (B → A) ] ((b : B) → f (r b) ≡ b)

  --

  data Two : Type lzero where
    p0 p1 : Two

  p0≢p1 : ¬ p0 ≡ p1
  p0≢p1 q = subst B q tt
    where
    B : Two → Type lzero
    B p0 = ⊤
    B p1 = ⊥

  -- Stuff for lib

  _>>=_ : ∀ {a b} {A : Set a} {B : Set b} → ∥ A ∥ → (A → ∥ B ∥) → ∥ B ∥
  x >>= f = recPropTrunc squash f x

  _<$>_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → ∥ A ∥ → ∥ B ∥
  f <$> x = x >>= (∣_∣ ∘ f)

  --

  Choice : ∀ {a b r} (A : Type a) (B : Type b) → (A → B → Type r) → Type (a ⊔ b ⊔ r)
  Choice A B R =
    ((a : A) → ∥ Σ[ b ∈ B ] R a b ∥) →
    ∥ Σ[ f ∈ (A → B) ] ((a : A) → R a (f a)) ∥

  Choice→IsSplitSurjection :
    ∀ {a b} (A : HSet a) (B : HSet b) {f : A .type → B .type} →
    Choice (B .type) (A .type) (λ b a → f a ≡ b) →
    IsSurjection f → IsSplitSurjection f
  Choice→IsSplitSurjection A B {f} choice surj =
    (λ { (f , p) b → f b , p b }) <$> choice surj

  --

  module WithProp (P : HProp lzero) where

    data Two/ : Type lzero where
      [_] : (b : Two) → Two/
      path : (p : P .type) → [ p0 ] ≡ [ p1 ]

    module _ {q} (Q : Two/ → HProp q) (let module Q b = HProp (Q b)) where

      Two/-elim-prop : (∀ b → Q.type [ b ]) → ∀ b → Q.type b
      Two/-elim-prop c [ b ] = c b
      Two/-elim-prop c (path x i) = eq i
        where
        eq : PathP (λ i → Q.type (path x i)) (c p0) (c p1)
        eq = isProp→PathP Q.isProp (path x) (c p0) (c p1)

    isSurjection : IsSurjection [_]
    isSurjection = Two/-elim-prop
      (λ b → record { isProp = propTruncIsProp })
      (λ b → ∣ b , refl ∣)

    surj : Surjection Two Two/
    surj = record
      { act = [_]
      ; isSurjection = isSurjection
      }

    --

    module WithP (p : P .type) where

      [p0]-IsCentre : ∀ b → [ p0 ] ≡ b
      [p0]-IsCentre [ p0 ] = refl
      [p0]-IsCentre [ p1 ] = path p
      [p0]-IsCentre (path p′ i) = eq i
        where
        eq′ : PathP (λ i → [ p0 ] ≡ path p′ i) refl (path p′)
        eq′ i j = path p′ (i ∧ j)

        eq : PathP (λ i → [ p0 ] ≡ path p′ i) refl (path p)
        eq = subst (λ z → PathP _ refl (path z)) (P .isProp p′ p) eq′

      Two/-IsContr : IsContr Two/
      Two/-IsContr = [ p0 ] , [p0]-IsCentre

      isStrongSurjection : IsStrongSurjection [_]
      isStrongSurjection b = p0 , [p0]-IsCentre b

    module With¬P (¬p : ¬ P .type) where

      [_]⁻¹ : Two/ → Two
      [ [ b ] ]⁻¹ = b
      [ path p i ]⁻¹ = eq i
        where
        eq : Path Two p0 p1
        eq = ⊥-elim (¬p p)

      [[]⁻¹] : ∀ b → [ [ b ]⁻¹ ] ≡ b
      [[]⁻¹] [ b ] = refl
      [[]⁻¹] (path p i) = eq i
        where
        eq : PathP (λ i → [ [ path p i ]⁻¹ ] ≡ path p i) refl refl
        eq = ⊥-elim (¬p p)

      Two/≡Two : Two/ ≡ Two
      Two/≡Two = isoToPath record
        { fun = [_]⁻¹
        ; inv = [_]
        ; rightInv = λ _ → refl
        ; leftInv = [[]⁻¹]
        }

      isStrongSurjection : IsStrongSurjection [_]
      isStrongSurjection b = [ b ]⁻¹ , [[]⁻¹] b

    em→isStrongSurjection : Dec (P .type) → IsStrongSurjection [_]
    em→isStrongSurjection (yes p) = WithP.isStrongSurjection p
    em→isStrongSurjection (no ¬p) = With¬P.isStrongSurjection ¬p

    --

    code : Two/ → Type lzero
    code [ p0 ] = ⊤
    code [ p1 ] = P .type
    code (path p i) = eq i
      where
      eq : ⊤ ≡ P .type
      eq = isoToPath record
        { fun = λ _ → p
        ; inv = _
        ; rightInv = P .isProp p
        ; leftInv = λ _ → refl
        }

    encode : ∀ {b} → [ p0 ] ≡ b → code b
    encode q = subst code q tt

    [p0]≡[p1]→p : [ p0 ] ≡ [ p1 ] → P .type
    [p0]≡[p1]→p = encode

    isStrongSurjection→em :
      IsStrongSurjection [_] → Dec (P .type)
    isStrongSurjection→em ss with ss [ p0 ] | ss [ p1 ]
                               | inspect ss [ p0 ] | inspect ss [ p1 ]
    isStrongSurjection→em ss | p0 , _ | p0 , q1 | _ | _ = yes ([p0]≡[p1]→p q1)
    isStrongSurjection→em ss | p0 , _ | p1 , _ | ≡p.[ ss0q ] | ≡p.[ ss1q ] =
      no (λ p → neq (path p))
      where
      ssq : ∀ b → proj₁ (ss [ b ]) ≡ b
      ssq p0 rewrite ≡p.cong proj₁ ss0q = refl
      ssq p1 rewrite ≡p.cong proj₁ ss1q = refl

      neq : ¬ [ p0 ] ≡ [ p1 ]
      neq [p0]=[p1] = p0≢p1 p0=p1
        where
        ss1=0 : proj₁ (ss [ p1 ]) ≡ p0
        ss1=0 = subst (λ z → proj₁ (ss z) ≡ p0) [p0]=[p1] (ssq p0)

        ss1=1 : proj₁ (ss [ p1 ]) ≡ p1
        ss1=1 = ssq p1

        p0=p1 : p0 ≡ p1
        p0=p1 = ss1=0 ⁻¹ ∙ ss1=1
    isStrongSurjection→em ss | p1 , q0 | _ | _ | _ = yes ([p0]≡[p1]→p (q0 ⁻¹))

    --

    Dec-IsProp : IsProp (Dec (P .type))
    Dec-IsProp (false because [¬p]) ( true because  [p]) =
      ⊥-elim (invert [¬p] (invert [p]))
    Dec-IsProp ( true because  [p]) (false because [¬p]) =
      ⊥-elim (invert [¬p] (invert [p]))
    Dec-IsProp (no ¬p) (no ¬p′) = cong no (funExt (λ p → ⊥-elim (¬p p)))
    Dec-IsProp (yes p) (yes p′) = cong yes (P .isProp p p′)

    choice→em : Choice Two/ Two (λ b a → [ a ] ≡ b) → Dec (P .type)
    choice→em choice = recPropTrunc
      Dec-IsProp
      (λ { (f , p) → isStrongSurjection→em (λ b → f b , p b) })
      (choice isSurjection)