# HG changeset patch # User Shinji KONO # Date 1591529352 -32400 # Node ID 5de8905a5a2b83d3a4a364fca1d881e450135cec # Parent 4ae48eed654a51d7bfac5c168c4731e302657a94 ... diff -r 4ae48eed654a -r 5de8905a5a2b LEMC.agda --- 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 diff -r 4ae48eed654a -r 5de8905a5a2b OD.agda --- 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∅ diff -r 4ae48eed654a -r 5de8905a5a2b filter.agda --- 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 = {!!}