Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 256:6e1c60866788 release
orderd pair and product
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Aug 2019 16:18:37 +0900 |
| parents | fe8392f527eb (current diff) 1eba96b7ab8d (diff) |
| children | 4fcac1eebc74 |
| files | |
| diffstat | 7 files changed, 264 insertions(+), 152 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgtags Mon Aug 12 09:04:16 2019 +0900 +++ b/.hgtags Thu Aug 29 16:18:37 2019 +0900 @@ -13,3 +13,5 @@ 2c7d45734e3be59a06d272a07fecdbf77ab8ce10 current 2c7d45734e3be59a06d272a07fecdbf77ab8ce10 current 1b1620e2053cfc340a4df0d63de65b9059b19b6f current +1b1620e2053cfc340a4df0d63de65b9059b19b6f current +2ea2a19f9cd638b29af51a47fa3dabdaea381d5c current
--- a/OD.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/OD.agda Thu Aug 29 16:18:37 2019 +0900 @@ -33,7 +33,7 @@ eq→ : ∀ { x : Ordinal } → def a x → def b x eq← : ∀ { x : Ordinal } → def b x → def a x -id : {n : Level} {A : Set n} → A → A +id : {A : Set n} → A → A id x = x eq-refl : { x : OD } → x == x @@ -171,6 +171,70 @@ is-o∅ x | tri≈ ¬a b ¬c = yes b is-o∅ x | tri> ¬a ¬b c = no ¬b +_,_ : OD → OD → OD +x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) +<_,_> : (x y : OD) → OD +< x , y > = (x , x ) , (x , y ) + +exg-pair : { x y : OD } → (x , y ) == ( y , x ) +exg-pair {x} {y} = record { eq→ = left ; eq← = right } where + left : {z : Ordinal} → def (x , y) z → def (y , x) z + left (case1 t) = case2 t + left (case2 t) = case1 t + right : {z : Ordinal} → def (y , x) z → def (x , y) z + right (case1 t) = case2 t + right (case2 t) = case1 t + +==-trans : { x y z : OD } → x == y → y == z → x == z +==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } + +==-sym : { x y : OD } → x == y → y == x +==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } + +ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y +ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) + +od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y +od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) + +eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > +eq-prod refl refl = refl + +prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) +prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where + lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y + lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) + lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b + lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) + lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y + lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where + lemma3 : ( x , x ) == ( y , z ) + lemma3 = ==-trans eq exg-pair + lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y + lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) + lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) + lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) + lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z + lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) + lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z + ... | refl with lemma2 (==-sym eq ) + ... | refl = refl + lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z + lemmax : x ≡ x' + lemmax with eq→ eq {od→ord (x , x)} (case1 refl) + lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') + lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' + ... | refl = lemma1 (ord→== s ) + lemmay : y ≡ y' + lemmay with lemmax + ... | refl with lemma4 eq -- with (x,y)≡(x,y') + ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) + ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p ppp {p} {a} d = d @@ -193,13 +257,13 @@ lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) -∋-p : ( p : Set n ) → Dec p -- assuming axiom of choice -∋-p p with p∨¬p p -∋-p p | case1 x = yes x -∋-p p | case2 x = no x +decp : ( p : Set n ) → Dec p -- assuming axiom of choice +decp p with p∨¬p p +decp p | case1 x = yes x +decp p | case2 x = no x double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic -double-neg-eilm {A} notnot with ∋-p A -- assuming axiom of choice +double-neg-eilm {A} notnot with decp A -- assuming axiom of choice ... | yes p = p ... | no ¬p = ⊥-elim ( notnot ¬p ) @@ -268,8 +332,6 @@ Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD → (OD → OD ) → OD Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } - _,_ : OD → OD → OD - x , y = Ord (omax (od→ord x) (od→ord y)) _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = record { def = λ x → def A x ∧ def B x } Union : OD → OD @@ -294,7 +356,8 @@ isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite isZF = record { isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } - ; pair = pair + ; pair→ = pair→ + ; pair← = pair← ; union→ = union→ ; union← = union← ; empty = empty @@ -311,9 +374,17 @@ ; choice = choice } where - pair : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) - proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) - proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) + pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) + pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) + + pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t + pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) + pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) + + -- pair0 : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) + -- proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) + -- proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) empty : (x : OD ) → ¬ (od∅ ∋ x) empty x = ¬x<0 @@ -477,10 +548,55 @@ choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimul A not -_,_ = ZF._,_ OD→ZF + --- + --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice + --- + record choiced ( X : OD) : Set (suc n) where + field + a-choice : OD + is-in : X ∋ a-choice + + choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X + choice-func' X p∨¬p not = have_to_find where + ψ : ( ox : Ordinal ) → Set (suc n) + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X + lemma-ord : ( ox : Ordinal ) → ψ ox + lemma-ord ox = TransFinite {ψ} induction ox where + ∋-p : (A x : OD ) → Dec ( A ∋ x ) + ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) + ∋-p A x | case1 (lift t) = yes t + ∋-p A x | case2 t = no (λ x → t (lift x )) + ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } + → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B + ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) + ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where + lemma : ¬ ((x : Ordinal ) → A x) → B + lemma not with p∨¬p B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x + induction x prev with ∋-p X ( ord→od x) + ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) + ... | no ¬p = lemma where + lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X + lemma1 y with ∋-p X (ord→od y) + lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) + lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X + lemma = ∀-imply-or lemma1 + have_to_find : choiced X + have_to_find with lemma-ord (od→ord X ) + have_to_find | t = dont-or t ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) + ¬¬X∋x nn = not record { + eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) + } + + Union = ZF.Union OD→ZF Power = ZF.Power OD→ZF Select = ZF.Select OD→ZF Replace = ZF.Replace OD→ZF isZF = ZF.isZF OD→ZF -TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
--- a/Ordinals.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/Ordinals.agda Thu Aug 29 16:18:37 2019 +0900 @@ -50,6 +50,7 @@ ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) + TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) o<-dom : { x y : Ordinal } → x o< y → Ordinal o<-dom {x} _ = x
--- a/cardinal.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/cardinal.agda Thu Aug 29 16:18:37 2019 +0900 @@ -20,40 +20,106 @@ open _∧_ open _∨_ open Bool +open _==_ -- we have to work on Ordinal to keep OD Level n -- since we use p∨¬p which works only on Level n +-- < x , y > = (x , x) , (x , y) + +data ord-pair : (p : Ordinal) → Set n where + pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) + +ZFProduct : OD +ZFProduct = record { def = λ x → ord-pair x } + +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y' +-- eq-pair refl refl = HE.refl + +pi1 : { p : Ordinal } → ord-pair p → Ordinal +pi1 ( pair x y) = x + +π1 : { p : OD } → ZFProduct ∋ p → Ordinal +π1 lt = pi1 lt + +pi2 : { p : Ordinal } → ord-pair p → Ordinal +pi2 ( pair x y ) = y + +π2 : { p : OD } → ZFProduct ∋ p → Ordinal +π2 lt = pi2 lt + +p-cons : ( x y : OD ) → ZFProduct ∋ < x , y > +p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( + let open ≡-Reasoning in begin + od→ord < ord→od (od→ord x) , ord→od (od→ord y) > + ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ + od→ord < x , y > + ∎ ) + + +p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > +p-iso1 {ox} {oy} = pair ox oy + +p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x +p-iso {x} p = ord≡→≡ (lemma p) where + lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op + lemma (pair ox oy) = refl + + +∋-p : (A x : OD ) → Dec ( A ∋ x ) +∋-p A x with p∨¬p ( A ∋ x ) +∋-p A x | case1 t = yes t +∋-p A x | case2 t = no t + +_⊗_ : (A B : OD) → OD +A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where + checkAB : { p : Ordinal } → def ZFProduct p → Set n + checkAB (pair x y) = def A x ∧ def B y + +func→od0 : (f : Ordinal → Ordinal ) → OD +func→od0 f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where + checkfunc : { p : Ordinal } → def ZFProduct p → Set n + checkfunc (pair x y) = f x ≡ y + +-- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) + +Func : ( A B : OD ) → OD +Func A B = record { def = λ x → def (Power (A ⊗ B)) x } + +-- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD -func→od f dom = Replace dom ( λ x → x , (ord→od (f (od→ord x) ))) - -record _⊗_ (A B : Ordinal) : Set n where - field - π1 : Ordinal - π2 : Ordinal - A∋π1 : def (ord→od A) π1 - B∋π2 : def (ord→od B) π2 +func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) --- Clearly wrong. We need ordered pair -Func : ( A B : OD ) → OD -Func A B = record { def = λ x → (od→ord A) ⊗ (od→ord B) } - -open _⊗_ +record Func←cd { dom cod : OD } {f : Ordinal } : Set n where + field + func-1 : Ordinal → Ordinal + func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom + +od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f} +od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where + lemma : Ordinal → Ordinal → Ordinal + lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) + lemma x y | p | no n = o∅ + lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) + lemma2 : {p : Ordinal} → ord-pair p → Ordinal + lemma2 (pair x1 y1) with decp ( x1 ≡ x) + lemma2 (pair x1 y1) | yes p = y1 + lemma2 (pair x1 y1) | no ¬p = o∅ + fod : OD + fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > ) -func←od : { dom cod : OD } → (f : OD ) → Func dom cod ∋ f → (Ordinal → Ordinal ) -func←od {dom} {cod} f lt x = sup-o ( λ y → lemma y ) where - lemma : Ordinal → Ordinal - lemma y with p∨¬p ( _⊗_.π1 lt ≡ x ) - lemma y | case1 refl = _⊗_.π2 lt - lemma y | case2 not = o∅ + +open Func←cd -- contra position of sup-o< -- -postulate - -- contra-position of mimimulity of supermum required in Cardinal - sup-x : ( Ordinal → Ordinal ) → Ordinal - sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) +-- postulate +-- -- contra-position of mimimulity of supermum required in Cardinal +-- sup-x : ( Ordinal → Ordinal ) → Ordinal +-- sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) ------------ -- @@ -68,7 +134,8 @@ ymap : Ordinal xfunc : def (Func X Y) xmap yfunc : def (Func Y X) ymap - onto-iso : {y : Ordinal } → (lty : def Y y ) → func←od (ord→od xmap) xfunc ( func←od (ord→od ymap) yfunc y ) ≡ y + onto-iso : {y : Ordinal } → (lty : def Y y ) → + func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y open Onto @@ -88,7 +155,7 @@ xfunc1 = {!!} zfunc : def (Func Z X) zmap zfunc = {!!} - onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od (ord→od xmap1) xfunc1 ( func←od (ord→od zmap) zfunc z ) ≡ z + onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func-1 (od→func xfunc1 ) (func-1 (od→func zfunc ) z ) ≡ z onto-iso1 = {!!}
--- a/filter.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/filter.agda Thu Aug 29 16:18:37 2019 +0900 @@ -1,8 +1,10 @@ open import Level -open import OD +open import Ordinals +module filter {n : Level } (O : Ordinals {n}) where + open import zf -open import ordinal -module filter ( n : Level ) where +open import logic +import OD open import Relation.Nullary open import Relation.Binary @@ -12,23 +14,28 @@ open import Relation.Binary.PropositionalEquality open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) -od = OD→ZF {n} - +open inOrdinal O +open OD O +open OD.OD -record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where +open _∧_ +open _∨_ +open Bool + +record Filter ( P max : OD ) : Set (suc n) where field - _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) - G : OD {suc n} + _⊇_ : OD → OD → Set n + G : OD G∋1 : G ∋ max - Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ max - Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q - Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( - ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) + Gmax : { p : OD } → P ∋ p → p ⊇ max + Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q + Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( + ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) -dense : {n : Level} → Set (suc (suc n)) -dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q )) +dense : Set (suc n) +dense = { D P p : OD } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q )) -record NatFilter {n : Level} ( P : Nat → Set n) : Set (suc n) where +record NatFilter ( P : Nat → Set n) : Set (suc n) where field GN : Nat → Set n GN∋1 : GN 0 @@ -46,16 +53,16 @@ -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) -Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n} -Pred {n} dom = record { - def = λ x → def dom x → Set n +Pred : ( Dom : OD ) → OD +Pred dom = record { + def = λ x → def dom x → {!!} } -Hω2 : {n : Level} → OD {suc n} -Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) } +Hω2 : OD +Hω2 = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) } -Hω2Filter : {n : Level} → Filter {n} Hω2 od∅ -Hω2Filter {n} = record { +Hω2Filter : Filter Hω2 od∅ +Hω2Filter = record { _⊇_ = _⊇_ ; G = {!!} ; G∋1 = {!!} @@ -64,17 +71,17 @@ ; Gcompat = {!!} } where P = Hω2 - _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) + _⊇_ : OD → OD → Set n _⊇_ = {!!} - G : OD {suc n} + G : OD G = {!!} G∋1 : G ∋ od∅ G∋1 = {!!} - Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ od∅ + Gmax : { p : OD } → P ∋ p → p ⊇ od∅ Gmax = {!!} - Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q + Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q Gless = {!!} - Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( - ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) + Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( + ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) Gcompat = {!!}
--- a/ordinal.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/ordinal.agda Thu Aug 29 16:18:37 2019 +0900 @@ -1,4 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} open import Level module ordinal where @@ -204,21 +203,6 @@ lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 --- we cannot prove this in intutionistic logic --- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p --- postulate --- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) --- → (exists : ¬ (∀ y → ¬ ( ψ y ) )) --- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) --- → p --- --- Instead we prove --- -TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) - → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) - → (exists : ¬ (∀ y → ¬ ( ψ y ) )) - → ¬ p -TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) open import Ordinals @@ -322,69 +306,3 @@ dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x dz<dz refl = s<refl - --- - --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice - --- - record choiced ( X : OD) : Set (suc (suc n)) where - field - a-choice : OD - is-in : X ∋ a-choice - - choice-func' : (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X - choice-func' X p∨¬p not = have_to_find where - ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n)) - ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X - lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox - lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where - ∋-p' : (A x : OD ) → Dec ( A ∋ x ) - ∋-p' A x with p∨¬p ( A ∋ x ) - ∋-p' A x | case1 t = yes t - ∋-p' A x | case2 t = no t - ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) } - → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B - ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x) - ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t - ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where - lemma : ¬ ((x : Ordinal {suc n}) → A x) → B - lemma not with p∨¬p B - lemma not | case1 b = b - lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) - caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) - caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) )) - caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) - caseΦ lx prev | no ¬p = lemma where - lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X) - lemma1 x with trio< x (ordinal lx (Φ lx)) - lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where - lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx) - lemma2 (case1 lt) = case1 lt - lemma1 x | tri< a ¬b ¬c | case2 found = case2 found - lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df ) - lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt )) - lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c )) - lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X - lemma = ∀-imply-or lemma1 - caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) ) - caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } ) - caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) - caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where - lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥ - lemma y lt with trio< y (ordinal lx x ) - lemma y lt | tri< a ¬b ¬c = not_found y a - lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p - lemma y lt | tri> ¬a ¬b c with osuc-≡< lt - lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) - lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) - caseOSuc lx x (case2 found) | no ¬p = case2 found - caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) → - ψ (record { lv = lx ; ord = OSuc lx x }) - caseOSuc1 lx x lt = caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl)) - have_to_find : choiced X - have_to_find with lemma-ord (od→ord X ) - have_to_find | t = dont-or t ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥) - ¬¬X∋x nn = not record { - eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) - ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) - } -
--- a/zf.agda Mon Aug 12 09:04:16 2019 +0900 +++ b/zf.agda Thu Aug 29 16:18:37 2019 +0900 @@ -22,8 +22,9 @@ : Set (suc (n ⊔ m)) where field isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ - -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) - pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) + -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t ≈ y) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) @@ -34,7 +35,7 @@ _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) _∪_ : ( A B : ZFSet ) → ZFSet - A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easer + A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easier ｛_｝ : ZFSet → ZFSet ｛ x ｝ = ( x , x ) infixr 200 _∈_