[Agda] Agda with the excluded middle is inconsistent ?

[herbelin]

Hi,

I worked a bit on Chung-Kil's proof. We can make it almost the same
proof pattern as when using impredicativity, basically building the Ω
combinator, as shown in file cantor1.agda below.

I also have a more direct variant of this proof (file cantor2.agda
below) but unfortunately, I could not succeed in telling Agda how to
check it (the proofs seems OK to me, but typing needs to remember that
some variable p has both type A and ¬A and I don't know how to hint
this to Agda).

Basically, the shortened proof shows that excluded-middle is morally
used only once, in hiding the antecedent of I at level Set1 in a case
analysis to Set:

  cantor : Set -> Set
  cantor a with exmid (invimageI a) -- invimageI is ∃x:Set->Set.(I x)=a
  cantor a | inl (invelmtI x y) = x a -> Empty
  cantor a | inr b = One

vs (in an impredicative system)

  cantor : Set -> Set
  cantor a = ∀ (x : Set -> Set) -> Eq1 (I x) a -> x a -> Empty

I think we should also notice that the proof uses excluded-middle in
Set1. I don't see how it could refute excluded-middle in Set0 since
the use of excluded-middle here is really about contributing to embed
some object in the Set1 level into the Set level.

Hugo

-------------- next part --------------
module cantor1 where

  data Empty : Set where

  data One : Set where
    one : One

  data coprod (A : Set1) (B : Set1) : Set1 where
    inl : ∀ (a : A) -> coprod A B
    inr : ∀ (b : B) -> coprod A B

  postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)

  data Eq1 {A : Set1} (x : A) : A -> Set1 where
    refleq1 : Eq1 x x

  data I : (Set -> Set) -> Set where

  data invimageI (a : Set) : Set1 where
    invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a

  cantor : Set -> Set
  cantor a with exmid (invimageI a)
  cantor a | inl (invelmtI x y) = x a -> Empty
  cantor a | inr b = One

  castRL : ∀ { A B } -> Eq1 A B -> B -> A
  castRL refleq1 a = a

  castLR : ∀ { A B } -> Eq1 A B -> A -> B
  castLR refleq1 a = a

  CANTOR : Set
  CANTOR = I cantor

  expand : ∀ a -> Eq1 (cantor (I a)) (a (I a) -> Empty)
  expand a with exmid (invimageI (I a))
  expand a | inl (invelmtI .a refleq1) = refleq1 -- Injectivity is used here
  expand a | inr b with b (invelmtI a refleq1)
  expand a | inr b | ()

  negate : Eq1 (cantor CANTOR) (cantor CANTOR -> Empty)
  negate = expand cantor
  -- Remark: Agda does not accept a direct definition of (expand cantor)

  cantorempty : cantor CANTOR -> Empty
  cantorempty p = castLR negate p p

  Ω : Empty
  Ω = cantorempty (castRL negate cantorempty)
-------------- next part --------------
module cantor2 where

  data Empty : Set where

  data One : Set where
    one : One

  data coprod (A : Set1) (B : Set1) : Set1 where
    inl : ∀ (a : A) -> coprod A B
    inr : ∀ (b : B) -> coprod A B

  postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)

  data Eq1 {A : Set1} (x : A) : A -> Set1 where
    refleq1 : Eq1 x x

  data I : (Set -> Set) -> Set where

  data invimageI (a : Set) : Set1 where
    invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a

  cantor : Set -> Set
  cantor a with exmid (invimageI a)
  cantor .(I x) | inl (invelmtI x refleq1) = x (I x) -> Empty
  cantor a | inr b = One

  CANTOR : Set
  CANTOR = I cantor

  yes : cantor CANTOR
  yes with exmid (invimageI CANTOR)
  yes | inl (invelmtI .cantor refleq1) = λ p -> p p
  yes | inr b = one

  no : cantor CANTOR -> Empty
  no p with exmid (invimageI CANTOR)
  no p | inl (invelmtI .cantor refleq1) = p p
  no p | inr b with b (invelmtI cantor refleq1)
  no p | inr b | ()

  Ω : Empty
  Ω = no yes