Berardi's paradox in Agda

Berardi.agda

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

module Berardi where

-- proof irrelevance from impredicativity and excluded middle
-- adapted from https://www.cs.princeton.edu/courses/archive/fall07/cos595/stdlib/html/Coq.Logic.Berardi.html

open import Agda.Primitive

{-# NO_UNIVERSE_CHECK #-}
record Impred (A : Set₁) (B : A → Set) : Set where
  field at : (a : A) → B a

data _⊎_ (A : Set) (B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

data ⊥ : Set where
void : ⊥ → {A : Set} → A
void ()

postulate EM : (A : Set) → A ⊎ (A → ⊥)

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

IFProp : {P : Set} (B : Set) (e1 e2 : P) → P
IFProp B e1 e2 with EM B
... | inl _ = e1
... | inr _ = e2

AC_IF : {P : Set} (B : Set) {e1 e2 : P} {Q : P → Set} → (B → Q e1) → ((B → ⊥) → Q e2) → Q (IFProp B e1 e2)
AC_IF B p1 p2 with EM B
... | inl b = p1 b
... | inr ¬b = p2 ¬b

data Bool : Set where
  T F : Bool

pow : Set → Set
pow P = P → Bool

module _ (A B : Set) where
  record retract : Set where
    field
      i : A → B
      j : B → A
      inv : (a : A) → j (i a) ≡ a
  open retract public

  record retract_cond : Set where
    field
      i2 : A → B
      j2 : B → A
      inv2 : retract → (a : A) → j2 (i2 a) ≡ a
  open retract_cond public

  AC : (r : retract_cond) → retract → (a : A) → j2 r (i2 r a) ≡ a
  AC r = r .inv2

L1 : (A B : Set) → retract_cond (pow A) (pow B)
L1 A B with EM (retract (pow A) (pow B))
... | inl r = record { i2 = retract.i r ; j2 = retract.j r ; inv2 = λ _ → retract.inv r }
... | inr ¬r = record { i2 = λ _ _ → F ; j2 = λ _ _ → F ; inv2 = λ r → void (¬r r) }

U : Set
U = Impred Set λ P → pow P

f : U → pow U
f u = u .Impred.at U

g : pow U → U
g h .Impred.at x = j2 (L1 x U) (i2 (L1 U U) h)

retract_pow_U_U : retract (pow U) U
retract_pow_U_U .i = g
retract_pow_U_U .j = f
retract_pow_U_U .inv a = AC (pow U) (pow U) (L1 U U) (record { i = λ x → x ; j = λ x → x ; inv = λ a₁ → refl }) a

Not_b : Bool → Bool
Not_b b = IFProp (b ≡ T) F T

R : U
R = g λ u → Not_b (u .Impred.at U u)

not_has_fixpoint : R .Impred.at U R ≡ Not_b (R .Impred.at U R)
not_has_fixpoint = ap (λ w → w R) (AC (pow U) (pow U) (L1 U U)
                                      (record { i = λ x → x ; j = λ x → x ; inv = λ a → refl })
                                      (λ u → Not_b (u .Impred.at U u)))

classical_proof_irrelevance : T ≡ F
-- classical_proof_irrelevance = AC_IF (R .Impred.at U R ≡ T) {Q = λ _ → T ≡ F} ? ?
classical_proof_irrelevance = helper not_has_fixpoint
  where
    helper : R .Impred.at U R ≡ Not_b (R .Impred.at U R) → T ≡ F
    helper not_has_fixpoint with EM (R .Impred.at U R ≡ T)
    ... | inl ≡T = trans (sym ≡T) not_has_fixpoint
    ... | inr ¬≡T = void (¬≡T not_has_fixpoint)