Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 308:b172ab9f12bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jun 2020 00:05:16 +0900
parents d5c5d87b72df
children d4802179a66f
comparison
equal deleted inserted replaced
307:d5c5d87b72df 308:b172ab9f12bc
76 76
77 record HOD : Set (suc n) where 77 record HOD : Set (suc n) where
78 field 78 field
79 od : OD 79 od : OD
80 odmax : Ordinal 80 odmax : Ordinal
81 <odmax : {x : Ordinal} → def od x → x o< odmax 81 <odmax : {y : Ordinal} → def od y → y o< odmax
82 82
83 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where 83 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
84 field 84 field
85 os→ : (x : Ordinal) → x o< maxordinal → Ordinal 85 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
86 os← : Ordinal → Ordinal 86 os← : Ordinal → Ordinal
120 lemma {x} lt = lt 120 lemma {x} lt = lt
121 121
122 od∅ : HOD 122 od∅ : HOD
123 od∅ = Ord o∅ 123 od∅ = Ord o∅
124 124
125 sup-od : ( HOD → HOD ) → HOD
126 sup-od = {!!}
127 sup-c< : ( ψ : HOD → HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
128 sup-c< = {!!}
129
130 odef : HOD → Ordinal → Set n 125 odef : HOD → Ordinal → Set n
131 odef A x = def ( od A ) x 126 odef A x = def ( od A ) x
132 127
133 o<→c<→HOD=Ord : ( {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x) 128 o<→c<→HOD=Ord : ( {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x)
134 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 129 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
142 137
143 _c<_ : ( x a : HOD ) → Set n 138 _c<_ : ( x a : HOD ) → Set n
144 x c< a = a ∋ x 139 x c< a = a ∋ x
145 140
146 cseq : {n : Level} → HOD → HOD 141 cseq : {n : Level} → HOD → HOD
147 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = {!!} } where 142 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
143 lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
144 lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
148 145
149 odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x 146 odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x
150 odef-subst df refl refl = df 147 odef-subst df refl refl = df
151 148
152 otrans : {n : Level} {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y 149 otrans : {n : Level} {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
153 otrans x<a y<x = ordtrans y<x x<a 150 otrans x<a y<x = ordtrans y<x x<a
154 151
155 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 152 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
156 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso 153 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso
157
158 154
159 -- avoiding lv != Zero error 155 -- avoiding lv != Zero error
160 orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y 156 orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y
161 orefl refl = refl 157 orefl refl = refl
162 158
210 is-o∅ x | tri< a ¬b ¬c = no ¬b 206 is-o∅ x | tri< a ¬b ¬c = no ¬b
211 is-o∅ x | tri≈ ¬a b ¬c = yes b 207 is-o∅ x | tri≈ ¬a b ¬c = yes b
212 is-o∅ x | tri> ¬a ¬b c = no ¬b 208 is-o∅ x | tri> ¬a ¬b c = no ¬b
213 209
214 _,_ : HOD → HOD → HOD 210 _,_ : HOD → HOD → HOD
215 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)) 211 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where
212 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
213 lemma {t} (case1 refl) = omax-x _ _
214 lemma {t} (case2 refl) = omax-y _ _
215
216 216
217 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 217 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
218 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 218 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
219 219
220 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD 220 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD
221 in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; odmax = {!!} ; <odmax = {!!} } 221 in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; odmax = {!!} ; <odmax = {!!} }
222 222
223 -- Power Set of X ( or constructible by λ y → odef X (od→ord y ) 223 -- Power Set of X ( or constructible by λ y → odef X (od→ord y )
224 224
225 ZFSubset : (A x : HOD ) → HOD 225 ZFSubset : (A x : HOD ) → HOD
226 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = {!!} ; <odmax = {!!} } -- roughly x = A → Set 226 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set
227 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
228 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
229
227 230
228 OPwr : (A : HOD ) → HOD 231 OPwr : (A : HOD ) → HOD
229 OPwr A = Ord ( sup-o A {!!} ) -- ( λ x → od→ord ( ZFSubset A x) ) ) 232 OPwr A = Ord ( sup-o A {!!} ) -- ( λ x → od→ord ( ZFSubset A x) ) )
230 233
231 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n 234 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n
273 ; infinite = infinite 276 ; infinite = infinite
274 ; isZF = isZF 277 ; isZF = isZF
275 } where 278 } where
276 ZFSet = HOD -- is less than Ords because of maxod 279 ZFSet = HOD -- is less than Ords because of maxod
277 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 280 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
278 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} } 281 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
279 Replace : HOD → (HOD → HOD ) → HOD 282 Replace : HOD → (HOD → HOD ) → HOD
280 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x)) 283 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
281 _∩_ : ( A B : ZFSet ) → ZFSet 284 _∩_ : ( A B : ZFSet ) → ZFSet
282 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = {!!} ; <odmax = {!!} } 285 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = {!!} ; <odmax = {!!} }
283 Union : HOD → HOD 286 Union : HOD → HOD
357 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 360 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
358 selection {ψ} {X} {y} = record { 361 selection {ψ} {X} {y} = record {
359 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 362 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
360 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 363 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
361 } 364 }
365 sup-od : ( HOD → HOD ) → HOD
366 sup-od = {!!}
367 sup-c< : ( ψ : HOD → HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
368 sup-c< = {!!}
362 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x 369 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x
363 replacement← {ψ} X x lt = record { proj1 = {!!} ; proj2 = lemma } where -- sup-c< ψ {x} 370 replacement← {ψ} X x lt = record { proj1 = {!!} ; proj2 = lemma } where -- sup-c< ψ {x}
364 lemma : odef (in-codomain X ψ) (od→ord (ψ x)) 371 lemma : odef (in-codomain X ψ) (od→ord (ψ x))
365 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 372 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
366 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) 373 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))