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
+