### changeset 287:5de8905a5a2b

...
author Shinji KONO Sun, 07 Jun 2020 20:29:12 +0900 4ae48eed654a 4fcac1eebc74 ef93c56ad311 LEMC.agda OD.agda filter.agda 3 files changed, 7 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
```--- a/LEMC.agda	Sun May 10 09:25:18 2020 +0900
+++ b/LEMC.agda	Sun Jun 07 20:29:12 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 ```
```--- a/OD.agda	Sun May 10 09:25:18 2020 +0900
+++ b/OD.agda	Sun Jun 07 20:29:12 2020 +0900
@@ -246,7 +246,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
@@ -260,7 +260,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∅```
```--- a/filter.agda	Sun May 10 09:25:18 2020 +0900
+++ b/filter.agda	Sun Jun 07 20:29:12 2020 +0900
@@ -43,8 +43,11 @@

open Filter

+L⊆L : (L : OD) → L ⊆ L
+L⊆L L = record { incl = λ {x} lt → lt }
+
L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
-L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!}
+L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!}

prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
@@ -83,7 +86,7 @@
import ordinal

-- open  ordinal.C-Ordinal-with-choice
-
+   -- both Power and infinite is too ZF, it is better to use simpler one
Hω2 : Filter (Power (Power infinite))
Hω2 = {!!}
```