# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595036192 -32400
# Node ID aad9249d1e8ff9c7572e7268636711489cdd227b
# Parent  8a430df110eb77ab60ec3a1759b2a942dad7a386
hω2

diff -r 8a430df110eb -r aad9249d1e8f OD.agda
--- 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
+
diff -r 8a430df110eb -r aad9249d1e8f OPair.agda
--- a/OPair.agda	Fri Jul 17 18:57:40 2020 +0900
+++ b/OPair.agda	Sat Jul 18 10:36:32 2020 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Ordinals
 module OPair {n : Level } (O : Ordinals {n})   where
diff -r 8a430df110eb -r aad9249d1e8f filter.agda
--- a/filter.agda	Fri Jul 17 18:57:40 2020 +0900
+++ b/filter.agda	Sat Jul 18 10:36:32 2020 +0900
@@ -6,14 +6,14 @@
 open import logic
 import OD 
 
-open import Relation.Nullary
-open import Relation.Binary
-open import Data.Empty
+open import Relation.Nullary 
+open import Relation.Binary 
+open import Data.Empty 
 open import Relation.Binary
 open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra
+import BAlgbra 
 
 open BAlgbra O
 
@@ -131,13 +131,6 @@
        dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
        dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
 
---    the set of finite partial functions from ω to 2
---
---   ph2 : Nat → Set → 2
---   ph2 : Nat → Maybe 2
---
--- Hω2 : Filter (Power (Power infinite))
-
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
        ideal : HOD   
@@ -153,3 +146,45 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
+--    the set of finite partial functions from ω to 2
+--
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
+-- Hω2 : Filter (Power (Power infinite))
+
+import OPair
+open OPair O
+
+ODSuc : (y : HOD) → infinite ∋ y → HOD
+ODSuc y lt = Union (y , (y , y)) 
+
+nat→ω : Nat → HOD
+nat→ω Zero = od∅
+nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+
+data Hω2 : ( x : Ordinal  ) → Set n where
+  hφ :  Hω2 o∅
+  h0 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 0 , ord→od x >)
+  h1 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 1 , ord→od x >)
+  h2 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 2 , ord→od x >)
+
+HODω2 :  HOD
+HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = {!!} ; <odmax = {!!} }
+
+-- the set of finite partial functions from ω to 2
+
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+Hω2f : Set (suc n)
+Hω2f = (Nat → Set n) → Two
+
+Hω2f→Hω2 : Hω2f  → HOD
+Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
+
+
diff -r 8a430df110eb -r aad9249d1e8f zf-in-agda.ind
--- a/zf-in-agda.ind	Fri Jul 17 18:57:40 2020 +0900
+++ b/zf-in-agda.ind	Sat Jul 18 10:36:32 2020 +0900
@@ -811,6 +811,17 @@
    odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (def A (od y) → def (od B) y)  → def (od A) x → def (od B) x
    odef-iso refl t = t
 
+--The uniqueness of HOD
+
+To prove extensionality or other we need ==→o≡.
+
+Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
+We can calculate the minimum using sup if we have bound but it is tedius.
+Only Select has non minimum odmax. 
+We have the same problem on 'def' itself, but we leave it, that is we assume the
+assumption of predicates of Agda have a unique form, it is something like the
+functional extensionality assumption.
+
 --Validity of Axiom of Extensionality
 
 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, 
@@ -915,7 +926,6 @@
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 
-
 --Axiom which have negation form
 
    Union, Selection