# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1591957274 -32400
# Node ID ef93c56ad3115a1ecb36197dde0848d6a4b4cd67
# Parent  359402cc6c3dcff2ba777c00165cd6cf157485a8# Parent  5de8905a5a2b83d3a4a364fca1d881e450135cec
...

diff -r 359402cc6c3d -r ef93c56ad311 LEMC.agda
--- a/LEMC.agda	Fri Jun 12 19:19:16 2020 +0900
+++ b/LEMC.agda	Fri Jun 12 19:21:14 2020 +0900
@@ -32,12 +32,6 @@
 
 open choiced
 
-double-neg-eilm : {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with p∨¬p A                         -- assuming axiom of choice
-... | case1 p = p
-... | case2 ¬p = ⊥-elim ( notnot ¬p )
-
-
 OD→ZFC : ZFC
 OD→ZFC   = record { 
     ZFSet = OD 
diff -r 359402cc6c3d -r ef93c56ad311 OD.agda
--- a/OD.agda	Fri Jun 12 19:19:16 2020 +0900
+++ b/OD.agda	Fri Jun 12 19:21:14 2020 +0900
@@ -256,7 +256,7 @@
     ; infinite = infinite
     ; isZF = isZF 
  } where
-    ZFSet = OD 
+    ZFSet = OD             -- is less than Ords because of maxod
     Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
@@ -270,7 +270,7 @@
     Power : OD  → OD 
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- ｛_｝ : ZFSet → ZFSet
-    -- ｛ x ｝ = ( x ,  x )
+    -- ｛ x ｝ = ( x ,  x )     -- it works but we don't use 
 
     data infinite-d  : ( x : Ordinal  ) → Set n where
         iφ :  infinite-d o∅
diff -r 359402cc6c3d -r ef93c56ad311 filter.agda