--- a/src/OD.agda	Mon Jan 01 18:21:36 2024 +0900
+++ b/src/OD.agda	Tue Jan 02 17:19:31 2024 +0900
@@ -260,9 +260,6 @@
    next-ord : Ordinal → Ordinal
    next-ord x = osuc x
 
-Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD
-Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
-
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
 
@@ -288,9 +285,16 @@
 --
 --
 
+ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
+ψiso {ψ} t refl = t
+
+*iso== : {y : HOD} → od y == od (* (& y))
+*iso== {y} = record { eq→ = λ {x} yx → eq← *iso yx ; eq← = λ {x} yx → eq→ *iso yx }
+
 record RCod (COD : HOD) (ψ : HOD → HOD)  : Set (suc n) where
  field
      ≤COD : ∀ {x : HOD } → ψ x ⊆ COD 
+     ψ-eq : ∀ {x y : HOD } → od x == od y  → ψ x ≡ ψ y 
 
 record Replaced (A : HOD) (ψ : Ordinal → Ordinal ) (x : Ordinal ) : Set n where
    field
@@ -307,7 +311,7 @@
             r01 = sym (Replaced.x=ψz lt )
 
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → {C : HOD} → (rc : RCod C ψ) → Replace X ψ rc ∋ ψ x
-replacement← {ψ} X x lt {C} rc = record { z = & x ; az = lt  ; x=ψz = cong (λ k → & (ψ k)) ? }
+replacement← {ψ} X x lt {C} rc = record { z = & x ; az = lt  ; x=ψz = cong (&) (RCod.ψ-eq rc *iso== ) }
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → {C : HOD} → (rc : RCod C ψ ) → (lt : Replace X ψ rc ∋ x) 
    →  ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x {C} rc lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
@@ -468,19 +472,34 @@
       lemma2 {y} record { owner = owner ; ao = case1 ao ; ox = ox } = record { owner = owner ; ao = case1 lemma4 ; ox = ox }  where
           lemma4 : owner ≡ & x
           lemma4 = trans ao ( ==→o≡ *iso )
-      lemma2 {y} record { owner = owner ; ao = case2 ao ; ox = ox } = record { owner = owner ; ao = case2 ? ; ox = ox }  where
-          lemma4 : owner ≡ & (x , x )
-          lemma4 = trans ao ( ==→o≡ record { eq→ = ? ; eq← = ? } )
+      lemma2 {y} record { owner = owner ; ao = case2 ao ; ox = ox } = record { owner = owner ; ao = case2 lemma4 ; ox = ox }  where
+          lemma4 : owner ≡ & (x , x) 
+          lemma4 = trans ao ( ==→o≡ record { eq→ = lemma5 _ ; eq← = lemma6 _ } ) where
+              lemma5 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x)
+              lemma5 y (case1 eq) = case1 (trans eq (sym (==→o≡ *iso== ) ))
+              lemma5 y (case2 eq) = case1 (trans eq (sym (==→o≡ *iso== ) ))
+              lemma6 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) 
+              lemma6 y (case1 eq) = case1 (trans eq ((==→o≡ *iso== ) ))
+              lemma6 y (case2 eq) = case1 (trans eq ((==→o≡ *iso== ) ))
       lemma3 :  {y : Ordinal}  → Own (x , (x , x)) y → Own (* (& x) , (* (& x) , * (& x))) y
-      lemma3 {y} record { owner = owner ; ao = ao ; ox = ox } = record { owner = owner ; ao = ? ; ox = ox } 
+      lemma3 {y} record { owner = owner ; ao = (case1 ao) ; ox = ox } = record { owner = owner 
+            ; ao = case1 (trans ao (==→o≡ *iso== )) ; ox = ox }
+      lemma3 {y} record { owner = owner ; ao = (case2 ao) ; ox = ox } = record { owner = owner 
+            ; ao = case2 (trans ao (==→o≡ record { eq→ = lemma5 _ ; eq← = lemma4 _  }))  ; ox = ox } where
+           lemma4 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x)
+           lemma4 y (case1 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) ))
+           lemma4 y (case2 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) ))
+           lemma5 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x)))
+           lemma5 y (case1 eq) = case1 ( trans eq ((==→o≡ *iso== ) ))
+           lemma5 y (case2 eq) = case1 ( trans eq ((==→o≡ *iso== ) ))
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
-pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) ? ? (o≡→== t≡x ))
-pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) ? ? (o≡→== t≡y ))
+pair→ x y t (case1 t≡x ) = case1 ( ord→== t≡x ) 
+pair→ x y t (case2 t≡y ) = case2 ( ord→== t≡y )
 
 pair← : ( x y t : HOD  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t
-pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) ?) -- (==→o≡ t=h=x))
-pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) ?) -- (==→o≡ t=h=y))
+pair← x y t (case1 t=h=x) = case1 (==→o≡ t=h=x)  
+pair← x y t (case2 t=h=y) = case2 (==→o≡ t=h=y)
 
 o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
 o<→c< lt {z} ox = ordtrans ox lt
@@ -492,16 +511,21 @@
 ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt  (o<-subst c (sym &iso) refl )
 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
 
-ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
-ψiso {ψ} t refl = t
-selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-selection {ψ} {X} {y} = ⟪
-     ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym ?)  ⟫ )
-  ,  ( λ select → ⟪ proj1 select  , ψiso {ψ} (proj2 select) ?  ⟫ )
-  ⟫
+open import zf
+
+Select : (X : HOD  ) → (ψ : (x : HOD  ) → Set n )  ( zψ : ZPred HOD _∋_ _=h=_ ψ ) → HOD
+Select X ψ zψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 
-selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y
-selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
+selection : {ψ : HOD → Set n} → { zψ : ZPred HOD _∋_ _=h=_ ψ } → { X y : HOD} →   ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ zψ ∋ y)
+selection {ψ} {zψ} {X} {y}   = ⟪
+     ( λ cond → ⟪ proj1 cond , peq  (proj2 cond) *iso==  ⟫ )
+  ,  ( λ select → ⟪ proj1 select  , peq (proj2 select) (==-sym *iso== )  ⟫ )
+  ⟫ where
+     peq : {x y : HOD } →  ψ x →  od x == od y  → ψ y
+     peq {x} {y} fx eq = proj1 (ZPred.ψ-cong zψ x y eq) fx
+
+selection-in-domain : {ψ : HOD → Set n} { zψ : ZPred HOD _∋_ _=h=_ ψ } {X y : HOD} → Select X ψ zψ ∋ y → X ∋ y
+selection-in-domain {ψ} {zψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {zψ} {X}  )) lt)
 
 ---
 --- Power Set
@@ -521,43 +545,24 @@
 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym &iso) (proj2 (eq (* x))) d
 
 extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
-proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ? d -- ( ==→o≡ (extensionality0 {A} {B} eq) ) d
-proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ? d -- (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
-
-open import zf
-
-record ODAxiom-sup : Set (suc n) where
- field
-  sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal -- required in Replace
-  sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } 
-     → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ
- sup-c≤ :  (ψ : HOD → HOD) → {X x : HOD} → def (od X) (& x)  → & (ψ x) o≤ (sup-o X (λ y X∋y → & (ψ (* y))))
- sup-c≤ ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) ? (sup-o≤ X lt )
+proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → odef w k) (==→o≡ (extensionality0 {A} {B} eq)) d
+proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → odef w k) (sym (==→o≡ (extensionality0 {A} {B} eq))) d
 
--- sup-o may contradict
---    If we have open monotonic function in Ordinal, there is no sup-o. 
---    for example, if we may have countable sequence of Ordinal, which contains some ordinal larger than any given Ordinal.
---    This happens when we have a coutable model. In this case, we have to have codomain restriction in  Replacement axiom.
---    that is, Replacement axiom does not create new ZF set.
-
-open ODAxiom-sup
-
-ZFReplace : ODAxiom-sup → HOD  → (HOD  → HOD) → HOD
-ZFReplace os X ψ = record { od = record { def = λ x → Replaced X (λ z → & (ψ (* z))) x  } ; odmax = rmax ; <odmax = rmax< } where
-        rmax : Ordinal
-        rmax = osuc ( sup-o os X (λ y X∋y → & (ψ (* y) )) )
-        rmax< :  {y : Ordinal} → Replaced X (λ z → & (ψ (* z))) y  → y o< rmax
-        rmax< {y} lt = subst (λ k → k o< rmax) r01 ( sup-o≤ os X (Replaced.az lt) ) where
+ZFReplace : HOD  → ( ψ : HOD  → HOD) →  ( ZFunc HOD _∋_ _=h=_ ψ )→ HOD
+ZFReplace X ψ zfψ = record { od = record { def = λ x → Replaced X (λ z → & (ψ (* z))) x  } ; odmax = & (ZFunc.cod zfψ) ; <odmax = rmax< } where
+        rmax< :  {y : Ordinal} → Replaced X (λ z → & (ψ (* z))) y → y o< & (ZFunc.cod zfψ)
+        rmax< {y} lt = subst (λ k → k o< & (ZFunc.cod zfψ) ) r01 (c<→o< (ZFunc.cod∋ψ zfψ (* (Replaced.z lt)) ) ) where
             r01 : & (ψ ( * (Replaced.z lt ) )) ≡ y
             r01 = sym (Replaced.x=ψz lt )
 
-zf-replacement← : (os : ODAxiom-sup) → {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → ZFReplace os X ψ ∋ ψ x
-zf-replacement← os {ψ} X x lt = record { z = & x ; az = lt  ; x=ψz = cong (λ k → & (ψ k)) (sym ?) }
-zf-replacement→ : (os : ODAxiom-sup ) → {ψ : HOD → HOD} (X x : HOD) → (lt : ZFReplace os X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
-zf-replacement→ os {ψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
+zf-replacement← :  {ψ : HOD → HOD} → {zfψ :  ZFunc HOD _∋_ _=h=_ ψ } → (X x : HOD) →  X ∋ x → ZFReplace X ψ zfψ ∋ ψ x
+zf-replacement← {ψ} {zfψ} X x lt = record { z = & x ; az = lt  ; x=ψz = ==→o≡  (ZFunc.ψ-cong zfψ _ _ *iso==  ) }
+zf-replacement→ : {ψ : HOD → HOD} → {zfψ : ZFunc HOD _∋_ _=h=_ ψ } → (X x : HOD) 
+     → (lt : ZFReplace X ψ zfψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
+zf-replacement→ {ψ} {zfψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
 
-isZF : (os : ODAxiom-sup)  (ho< : ODAxiom-ho< ) → IsZF HOD _∋_  _=h=_ od∅ _,_ Union Power Select (ZFReplace os) (Omega ho<)
-isZF os ho< = record {
+isZF :  (ho< : ODAxiom-ho< ) → IsZF HOD _∋_  _=h=_ od∅ _,_ Union Power Select ZFReplace (Omega ho<)
+isZF ho< = record {
         isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
     ;   pair→  = pair→
     ;   pair←  = pair←
@@ -570,13 +575,13 @@
     ;   ε-induction = ε-induction
     ;   infinity∅ = infinity∅ ho<
     ;   infinity = infinity ho<
-    ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-    ;   replacement← = zf-replacement← os
-    ;   replacement→ = λ {ψ} → zf-replacement→ os {ψ}
+    ;   selection = λ {X} {ψ} {zψ} {y} → selection {X} {ψ} {zψ} {y} 
+    ;   replacement← = λ {ψ} {zfψ} → zf-replacement← {ψ} {zfψ} 
+    ;   replacement→ = λ {ψ} {zfψ} → zf-replacement→ {ψ} {zfψ} 
     }
 
-HOD→ZF : ODAxiom-sup →  ODAxiom-ho< → ZF
-HOD→ZF os ho< = record {
+HOD→ZF : ODAxiom-ho< → ZF
+HOD→ZF ho< = record {
     ZFSet = HOD
     ; _∋_ = _∋_
     ; _≈_ = _=h=_
@@ -585,9 +590,9 @@
     ; Union = Union
     ; Power = Power
     ; Select = Select
-    ; Replace = ZFReplace os
+    ; Replace = ZFReplace 
     ; infinite = Omega ho<
-    ; isZF = isZF os ho<
+    ; isZF = isZF ho<
  }