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

comparison OD.agda @ 363:aad9249d1e8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hω2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Jul 2020 10:36:32 +0900
parents 4cbcf71b09c4
children 67580311cc8e
comparison
equal deleted inserted replaced
362:8a430df110eb 363:aad9249d1e8f
104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ 104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
105 105
106 postulate odAxiom : ODAxiom 106 postulate odAxiom : ODAxiom
107 open ODAxiom odAxiom 107 open ODAxiom odAxiom
108 108
109 -- odmax minimality
110 --
111 -- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
112 -- We can calculate the minimum using sup but it is tedius.
113 -- Only Select has non minimum odmax.
114 -- We have the same problem on 'def' itself, but we leave it.
115
116 odmaxmin : Set (suc n)
117 odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z
118
109 -- possible order restriction 119 -- possible order restriction
110 hod-ord< : {x : HOD } → Set n 120 hod-ord< : {x : HOD } → Set n
111 hod-ord< {x} = od→ord x o< next (odmax x) 121 hod-ord< {x} = od→ord x o< next (odmax x)
112 122
113 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD 123 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
318 328
319 HOD→ZF : ZF 329 HOD→ZF : ZF
320 HOD→ZF = record { 330 HOD→ZF = record {
321 ZFSet = HOD 331 ZFSet = HOD
322 ; _∋_ = _∋_ 332 ; _∋_ = _∋_
323 ; _≈_ = _=h=_ 333 ; _≈_ = hod→zf._=h=_
324 ; ∅ = od∅ 334 ; ∅ = od∅
325 ; _,_ = _,_ 335 ; _,_ = _,_
326 ; Union = Union 336 ; Union = hod→zf.Union
327 ; Power = Power 337 ; Power = hod→zf.Power
328 ; Select = Select 338 ; Select = hod→zf.Select
329 ; Replace = Replace 339 ; Replace = hod→zf.Replace
330 ; infinite = infinite 340 ; infinite = hod→zf.infinite
331 ; isZF = isZF 341 ; isZF = hod→zf.isZF
332 } where 342 } where
343 module hod→zf where
333 ZFSet = HOD -- is less than Ords because of maxod 344 ZFSet = HOD -- is less than Ords because of maxod
334 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 345 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
335 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 346 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
336 Replace : HOD → (HOD → HOD) → HOD 347 Replace : HOD → (HOD → HOD) → HOD
337 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } 348 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
408 lemma71 = next< lemma81 lemma9 419 lemma71 = next< lemma81 lemma9
409 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) 420 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
410 lemma1 = ho< 421 lemma1 = ho<
411 lemma2 : od→ord (u y) o< next o∅ 422 lemma2 : od→ord (u y) o< next o∅
412 lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) 423 lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
413 424
425 nat→ω : Nat → HOD
426 nat→ω Zero = od∅
427 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
428
429 ω→nat : (n : HOD) → infinite ∋ n → Nat
430 ω→nat n = lemma where
431 lemma : {y : Ordinal} → infinite-d y → Nat
432 lemma iφ = Zero
433 lemma (isuc lt) = Suc (lemma lt)
414 434
415 _=h=_ : (x y : HOD) → Set n 435 _=h=_ : (x y : HOD) → Set n
416 x =h= y = od x == od y 436 x =h= y = od x == od y
417 437
418 infixr 200 _∈_ 438 infixr 200 _∈_
654 674
655 Union = ZF.Union HOD→ZF 675 Union = ZF.Union HOD→ZF
656 Power = ZF.Power HOD→ZF 676 Power = ZF.Power HOD→ZF
657 Select = ZF.Select HOD→ZF 677 Select = ZF.Select HOD→ZF
658 Replace = ZF.Replace HOD→ZF 678 Replace = ZF.Replace HOD→ZF
679 infinite = ZF.infinite HOD→ZF
659 isZF = ZF.isZF HOD→ZF 680 isZF = ZF.isZF HOD→ZF
681