Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 304:2c111bfcc89a
HOD using <maxod
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jun 2020 18:31:56 +0900 |
| parents | 7963b76df6e1 |
| children | 4804f3f3485f |
line wrap: on
line diff
--- a/OD.agda Mon Jun 29 17:56:06 2020 +0900 +++ b/OD.agda Mon Jun 29 18:31:56 2020 +0900 @@ -77,7 +77,8 @@ record HOD : Set (suc n) where field od : OD - ¬odmax : ¬ (od ≡ Ords) + odmax : Ordinal + <odmax : {x : Ordinal} → def od x → x o< odmax record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where field @@ -89,12 +90,9 @@ open HOD --- HOD→OD : {x : Ordinal} → HOD x → OD --- HOD→OD hod = record { def = hdef {!!} } - record ODAxiom : Set (suc n) where - -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) field + -- HOD is isomorphic to Ordinal (by means of Goedel number) od→ord : HOD → Ordinal ord→od : Ordinal → HOD c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y @@ -114,22 +112,23 @@ -- maxod : {x : OD} → od→ord x o< od→ord Ords -- maxod {x} = c<→o< OneObj --- we have to avoid this contradiction - +-- we have not this contradiction -- bad-bad : ⊥ --- bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj) +-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One }; <odmax = {!!} } } OneObj) -- Ordinal in OD ( and ZFSet ) Transitive Set Ord : ( a : Ordinal ) → HOD -Ord a = record { od = record { def = λ y → y o< a } ; ¬odmax = ? } +Ord a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where + lemma : {x : Ordinal} → x o< a → x o< a + lemma {x} lt = lt od∅ : HOD od∅ = Ord o∅ sup-o : ( HOD → Ordinal ) → Ordinal -sup-o = ? +sup-o = {!!} sup-o< : { ψ : HOD → Ordinal } → ∀ {x : HOD } → ψ x o< sup-o ψ -sup-o< = ? +sup-o< = {!!} odef : HOD → Ordinal → Set n odef A x = def ( od A ) x @@ -148,7 +147,7 @@ x c< a = a ∋ x cseq : {n : Level} → HOD → HOD -cseq x = record { od = record { def = λ y → odef x (osuc y) } ; ¬odmax = ? } where +cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = {!!} ; <odmax = {!!} } where odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x odef-subst df refl refl = df @@ -216,18 +215,18 @@ is-o∅ x | tri> ¬a ¬b c = no ¬b _,_ : HOD → HOD → HOD -x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; ¬odmax = ? } -- Ord (omax (od→ord x) (od→ord y)) +x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = {!!} ; <odmax = {!!} } -- Ord (omax (od→ord x) (od→ord y)) -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD -in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; ¬odmax = ? } +in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; odmax = {!!} ; <odmax = {!!} } -- Power Set of X ( or constructible by λ y → odef X (od→ord y ) ZFSubset : (A x : HOD ) → HOD -ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; ¬odmax = ? } -- roughly x = A → Set +ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = {!!} ; <odmax = {!!} } -- roughly x = A → Set OPwr : (A : HOD ) → HOD OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) @@ -279,13 +278,13 @@ } where ZFSet = HOD -- is less than Ords because of maxod Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD - Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; ¬odmax = ? } + Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} } Replace : HOD → (HOD → HOD ) → HOD - Replace X ψ = record { od = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; ¬odmax = ? } + Replace X ψ = record { od = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } _∩_ : ( A B : ZFSet ) → ZFSet - A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; ¬odmax = ? } + A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = {!!} ; <odmax = {!!} } Union : HOD → HOD - Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; ¬odmax = ? } + Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} } _∈_ : ( A B : ZFSet ) → Set n A ∈ B = B ∋ A Power : HOD → HOD @@ -299,7 +298,7 @@ infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) infinite : HOD - infinite = record { od = record { def = λ x → infinite-d x } ; ¬odmax = ? } + infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} } _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y @@ -364,7 +363,7 @@ ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } } replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = record { proj1 = ? ; proj2 = lemma } where -- sup-c< ψ {x} + replacement← {ψ} X x lt = record { proj1 = {!!} ; proj2 = lemma } where -- sup-c< ψ {x} lemma : odef (in-codomain X ψ) (od→ord (ψ x)) lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))