<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META content="text/html; charset=ks_c_5601-1987" http-equiv=Content-Type>
<META name=GENERATOR content="MSHTML 8.00.6001.18854">
<STYLE></STYLE>
</HEAD>
<BODY bgColor=#ffffff>
<DIV><FONT size=2 face=Arial>Hi everyone,</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>I proved the absurdity in Agda assuming the 
excluded middle.</FONT></DIV>
<DIV><FONT size=2 face=Arial>Is it a well-known fact ?</FONT></DIV>
<DIV><FONT size=2 face=Arial>It seems that Agda's set theory is 
weird.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>This comes from the injectivity of inductive type 
constructors.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>The proof sketch is as follows.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>Define a family of inductive type</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>data I : (Set -&gt; Set) -&gt; 
Set&nbsp;where</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>with no constructors.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>By injectivity of type constructors, I can show 
that I : (Set -&gt; Set) -&gt; Set is injective.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>As you may see, there is a size problem with this 
injectivity.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>So, I just used the cantor's diagonalization to 
derive absurdity in a&nbsp;classical way.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>Does anyone know whether cantor's diagonalization 
essentially needs the classical axiom, or can be done intuitionistically 
?</FONT></DIV>
<DIV><FONT size=2 face=Arial>If the latter is true, then Agda system is 
inconsistent.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>Please have a look at the Agda code 
below.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>Any comments are wellcome.</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>Best regards,</FONT></DIV>
<DIV><FONT size=2 face=Arial>Chung-Kil Hur</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>============== Agda code 
===============</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>module cantor where</FONT></DIV>
<DIV><FONT size=2></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data Empty : Set where</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data One : Set where<BR>&nbsp;&nbsp;&nbsp; 
one : One</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data coprod (A : Set1) (B : Set1) : Set1 
where<BR>&nbsp;&nbsp;&nbsp; inl : ¢£ (a : A) -&gt; coprod A 
B<BR>&nbsp;&nbsp;&nbsp; inr : ¢£ (b : B) -&gt; coprod A B </FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; postulate exmid : ¢£ (A : Set1) -&gt; coprod 
A (A -&gt; Empty)</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data Eq1 {A : Set1} (x : A) : A -&gt; Set1 
where<BR>&nbsp;&nbsp;&nbsp; refleq1 : Eq1 x x</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; cast : ¢£ { A B } -&gt; Eq1 A B -&gt; A -&gt; 
B<BR>&nbsp; cast refleq1 a = a</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; Eq1cong : ¢£ {f g : Set -&gt; Set} a -&gt; 
Eq1 f g -&gt; Eq1 (f a) (g a)<BR>&nbsp; Eq1cong a refleq1 = refleq1</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; Eq1sym : ¢£ {A : Set1} { x y : A } -&gt; Eq1 
x y -&gt; Eq1 y x<BR>&nbsp; Eq1sym refleq1 = refleq1</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; Eq1trans : ¢£ {A : Set1} { x y z : A } -&gt; 
Eq1 x y -&gt; Eq1 y z -&gt; Eq1 x z<BR>&nbsp; Eq1trans refleq1 refleq1 = 
refleq1</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data I : (Set -&gt; Set) -&gt; Set 
where</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; Iinj : ¢£ { x y : Set -&gt; Set } -&gt; Eq1 
(I x) (I y) -&gt; Eq1 x y <BR>&nbsp; Iinj refleq1 = refleq1</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data invimageI (a : Set) : Set1 
where<BR>&nbsp;&nbsp;&nbsp; invelmtI : forall x -&gt; (Eq1 (I x) a) -&gt; 
invimageI a</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; J : Set -&gt; (Set -&gt; Set)<BR>&nbsp; J a 
with exmid (invimageI a)<BR>&nbsp; J a | inl (invelmtI x y) = x<BR>&nbsp; J a | 
inr b = ¥ë x ¡æ Empty</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; data invimageJ (x : Set -&gt; Set) : Set1 
where<BR>&nbsp;&nbsp;&nbsp; invelmtJ : forall a -&gt; (Eq1 (J a) x) -&gt; 
invimageJ x</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; IJIeqI : ¢£ x -&gt; Eq1 (I (J (I x))) (I 
x)<BR>&nbsp; IJIeqI x with exmid (invimageI (I x))<BR>&nbsp; IJIeqI x | inl 
(invelmtI x' y) = y<BR>&nbsp; IJIeqI x | inr b with b (invelmtI x 
refleq1)<BR>&nbsp; IJIeqI x | inr b | ()</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; J_srj : ¢£ (x : Set -&gt; Set) -&gt; 
invimageJ x<BR>&nbsp; J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; cantor : Set -&gt; Set<BR>&nbsp; cantor a 
with exmid (Eq1 (J a a) Empty)<BR>&nbsp; cantor a | inl a' = One<BR>&nbsp; 
cantor a | inr b = Empty</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; OneNeqEmpty : Eq1 One Empty -&gt; 
Empty<BR>&nbsp; OneNeqEmpty p = cast p one</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; cantorone : ¢£ a -&gt; Eq1 (J a a) Empty 
-&gt; Eq1 (cantor a) One <BR>&nbsp; cantorone a p with exmid (Eq1 (J a a) 
Empty)<BR>&nbsp; cantorone a p | inl a' = refleq1<BR>&nbsp; cantorone a p | inr 
b with b p<BR>&nbsp; cantorone a p | inr b | ()</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; cantorempty : ¢£ a -&gt; (Eq1 (J a a) Empty 
-&gt; Empty) -&gt; Eq1 (cantor a) Empty<BR>&nbsp; cantorempty a p with exmid 
(Eq1 (J a a) Empty)<BR>&nbsp; cantorempty a p | inl a' with p a'<BR>&nbsp; 
cantorempty a p | inl a' | ()<BR>&nbsp; cantorempty a p | inr b = 
refleq1</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; cantorcase : ¢£ a -&gt; Eq1 cantor (J a) 
-&gt; Empty<BR>&nbsp; cantorcase a pf with exmid (Eq1 (J a a) Empty)<BR>&nbsp; 
cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a 
a')) (Eq1cong a pf)) a')<BR>&nbsp; cantorcase a pf | inr b = b (Eq1trans (Eq1sym 
(Eq1cong a pf)) (cantorempty a b))</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>&nbsp; absurd : Empty<BR>&nbsp; absurd with (J_srj 
cantor)<BR>&nbsp; absurd | invelmtJ a y = cantorcase a (Eq1sym y)</FONT></DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial>=====================================</FONT></DIV>
<DIV>&nbsp;</DIV>
<DIV><FONT size=2 face=Arial></FONT>&nbsp;</DIV></BODY></HTML>