Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 363:aad9249d1e8f
hω2
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 18 Jul 2020 10:36:32 +0900 |
parents | 4cbcf71b09c4 |
children | 67580311cc8e |
line wrap: on
line diff
--- a/OD.agda Fri Jul 17 18:57:40 2020 +0900 +++ b/OD.agda Sat Jul 18 10:36:32 2020 +0900 @@ -106,6 +106,16 @@ postulate odAxiom : ODAxiom open ODAxiom odAxiom +-- odmax minimality +-- +-- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD. +-- We can calculate the minimum using sup but it is tedius. +-- Only Select has non minimum odmax. +-- We have the same problem on 'def' itself, but we leave it. + +odmaxmin : Set (suc n) +odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z + -- possible order restriction hod-ord< : {x : HOD } → Set n hod-ord< {x} = od→ord x o< next (odmax x) @@ -320,16 +330,17 @@ HOD→ZF = record { ZFSet = HOD ; _∋_ = _∋_ - ; _≈_ = _=h=_ + ; _≈_ = hod→zf._=h=_ ; ∅ = od∅ ; _,_ = _,_ - ; Union = Union - ; Power = Power - ; Select = Select - ; Replace = Replace - ; infinite = infinite - ; isZF = isZF + ; Union = hod→zf.Union + ; Power = hod→zf.Power + ; Select = hod→zf.Select + ; Replace = hod→zf.Replace + ; infinite = hod→zf.infinite + ; isZF = hod→zf.isZF } where + module hod→zf 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 = odmax X ; <odmax = λ y → <odmax X (proj1 y) } @@ -410,7 +421,16 @@ lemma1 = ho< lemma2 : od→ord (u y) o< next o∅ 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)) - + + nat→ω : Nat → HOD + nat→ω Zero = od∅ + nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) + + ω→nat : (n : HOD) → infinite ∋ n → Nat + ω→nat n = lemma where + lemma : {y : Ordinal} → infinite-d y → Nat + lemma iφ = Zero + lemma (isuc lt) = Suc (lemma lt) _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y @@ -656,4 +676,6 @@ Power = ZF.Power HOD→ZF Select = ZF.Select HOD→ZF Replace = ZF.Replace HOD→ZF +infinite = ZF.infinite HOD→ZF isZF = ZF.isZF HOD→ZF +