# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1684574902 -32400
# Node ID 302cfb533201cb79a60777849bbb58e71db5a59c
# Parent  45cd80181a293bb12846f95e4a74496bcc341c0f
fix Replacement

diff -r 45cd80181a29 -r 302cfb533201 src/OD.agda
--- a/src/OD.agda	Sat May 20 09:48:37 2023 +0900
+++ b/src/OD.agda	Sat May 20 18:28:22 2023 +0900
@@ -73,7 +73,7 @@
 --  bound on each HOD.
 --
 --  In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
---  we need explict assumption on sup.
+--  we need explict assumption on sup for unrestricted Replacement.
 --
 --  ==→o≡ is necessary to prove axiom of extensionality.
 
@@ -101,21 +101,20 @@
   *iso   :  {x : HOD }      → * ( & x ) ≡ x
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
-  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 ψ
   ∋-irr : {X : HOD} {x : Ordinal } → (a b : def (od X) x) → a ≅ b
--- possible order restriction (required in the axiom of infinite )
-  ho< : {x : HOD} → & x o< next (odmax x)
-
--- 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.
 
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
+-- possible order restriction (required in the axiom of infinite )
+
+record ODAxiom-ho< : Set (suc n) where
+ field
+  ho< : {x : HOD} → & x o< next (odmax x)
+
+postulate  odAxiom-ho< : ODAxiom-ho<
+open ODAxiom-ho< odAxiom-ho<
+
 -- odmax minimality
 --
 -- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
@@ -349,49 +348,59 @@
 union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
 union← X z UX∋z not = ⊥-elim ( not (* (Own.owner UX∋z)) ⟪ subst (λ k → odef X k) (sym &iso) ( Own.ao UX∋z) , Own.ox UX∋z ⟫  )
 
+record RCod (COD : HOD) (ψ : HOD → HOD)  : Set (suc n) where
+ field
+     ≤COD : ∀ {x : HOD } → ψ x ⊆ COD 
+
 record Replaced (A : HOD) (ψ : Ordinal → Ordinal ) (x : Ordinal ) : Set n where
    field
       z : Ordinal
       az : odef A z
       x=ψz  : x ≡ ψ z 
 
-Replace : HOD  → (HOD  → HOD) → HOD
-Replace X ψ = record { od = record { def = λ x → Replaced X (λ z → & (ψ (* z))) x  } ; odmax = rmax ; <odmax = rmax< } where
-        rmax : Ordinal
-        rmax = osuc ( sup-o 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≤ X (Replaced.az lt) ) where
+Replace : (D : HOD) → (ψ : HOD  → HOD) → {C : HOD} → RCod C ψ  → HOD
+Replace X ψ {C} rc = record { od = record { def = λ x → Replaced X (λ z → & (ψ (* z))) x  } ; odmax = osuc (& C)
+   ; <odmax = rmax< } where
+        rmax< :  {y : Ordinal} → Replaced X (λ z → & (ψ (* z))) y  → y o< osuc (& C)
+        rmax< {y} lt = subst (λ k → k o< osuc (& C)) r01 ( ⊆→o≤ (RCod.≤COD rc) ) where 
             r01 : & (ψ ( * (Replaced.z lt ) )) ≡ y
             r01 = sym (Replaced.x=ψz lt )
 
-replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = record { z = & x ; az = lt  ; x=ψz = cong (λ k → & (ψ k)) (sym *iso) }
-replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
-replacement→ {ψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (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)) (sym *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)) 
 
 --
 -- If we have LEM, Replace' is equivalent to Replace
 --
 
+record RXCod (X COD : HOD) (ψ : (x : HOD) → X ∋ x → HOD)  : Set (suc n) where
+ field
+     ≤COD : ∀ {x : HOD } → (lt : X ∋ x) → ψ x lt ⊆ COD 
+
 record Replaced1 (A : HOD) (ψ : (x : Ordinal ) → odef A x → Ordinal ) (x : Ordinal ) : Set n where
    field
       z : Ordinal
       az : odef A z
       x=ψz  : x ≡ ψ z az
 
-Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD
-Replace' X ψ = record { od = record { def = λ x → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) x  } ; odmax = rmax ; <odmax = rmax< } where
-        rmax : Ordinal
-        rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) )) )
-        rmax< :  {y : Ordinal} → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) y  → y o< rmax
-        rmax< {y} lt = subst (λ k → k o< rmax) r01 ( sup-o≤ X (Replaced1.az lt) ) where
+Replace' : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → {C : HOD} → RXCod X C ψ  → HOD
+Replace' X ψ {C} rc = record { od = record { def = λ x → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) x  } ; odmax = osuc (& C) ; <odmax = rmax< } where
+        rmax< :  {y : Ordinal} → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) y  → y o< osuc (& C)
+        rmax< {y} lt = subst (λ k → k o< osuc (& C)) r01 ( ⊆→o≤ (RXCod.≤COD rc (subst (λ k → odef X k) (sym &iso) (Replaced1.az lt) )))  where 
             r01 : & (ψ ( * (Replaced1.z lt ) ) (subst (λ k → odef X k) (sym &iso) (Replaced1.az lt) )) ≡ y
             r01 = sym (Replaced1.x=ψz lt )
 
+cod-conv : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → {C : HOD} → (rc : RXCod X C ψ   )
+      → RXCod (* (& X)) C (λ y xy → ψ y (subst (λ k → k ∋ y) *iso xy))
+cod-conv X ψ {C} rc = record { ≤COD = λ {x} lt → RXCod.≤COD rc (subst (λ k → odef k (& x)) *iso lt) }
 
-Replace'-iso : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → 
-      Replace' (* (& X)) (λ y xy → ψ y (subst (λ k → k ∋ y ) *iso xy) ) ≡ Replace' X ( λ y xy → ψ y xy ) 
-Replace'-iso X ψ = ==→o≡ record { eq→ = ri0 ; eq← = ri1 } where
+Replace'-iso : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → {C : HOD} → (rc : RXCod X C ψ   )
+      → Replace' (* (& X)) (λ y xy → ψ y (subst (λ k → k ∋ y ) *iso xy) ) (cod-conv X ψ rc)
+         ≡ Replace' X ( λ y xy → ψ y xy ) rc 
+Replace'-iso X ψ rc = ==→o≡ record { eq→ = ri0 ; eq← = ri1 } where
     ri2 : {z : Ordinal } (a b : X ∋ (* z)) → & (ψ (* z) a) ≡ & (ψ (* z) b)
     ri2 {z} a b = cong (λ k → & (ψ (* z) k)) ( HE.≅-to-≡ ( ∋-irr {X} {& (* z)} a b ) )
     ri0 : {x : Ordinal} 
@@ -506,9 +515,6 @@
 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)
 
-sup-c≤ :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o≤ (sup-o X (λ y X∋y → & (ψ (* y))))
-sup-c≤ ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o≤ X lt )
-
 ---
 --- Power Set
 ---
@@ -548,8 +554,38 @@
 
 open import zf
 
-isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
-isZF = record {
+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< _ ) *iso (sup-o≤ X lt )
+
+-- 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
+            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 *iso) }
+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)) 
+
+isZF : (os : ODAxiom-sup) → IsZF HOD _∋_  _=h=_ od∅ _,_ Union Power Select (ZFReplace os) infinite
+isZF os = record {
         isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
     ;   pair→  = pair→
     ;   pair←  = pair←
@@ -563,12 +599,12 @@
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
     ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-    ;   replacement← = replacement←
-    ;   replacement→ = λ {ψ} → replacement→ {ψ}
+    ;   replacement← = zf-replacement← os
+    ;   replacement→ = λ {ψ} → zf-replacement→ os {ψ}
     }
 
-HOD→ZF : ZF
-HOD→ZF   = record {
+HOD→ZF : ODAxiom-sup → ZF
+HOD→ZF os  = record {
     ZFSet = HOD
     ; _∋_ = _∋_
     ; _≈_ = _=h=_
@@ -577,9 +613,9 @@
     ; Union = Union
     ; Power = Power
     ; Select = Select
-    ; Replace = Replace
+    ; Replace = ZFReplace os
     ; infinite = infinite
-    ; isZF = isZF
+    ; isZF = isZF os
  }
 
 
diff -r 45cd80181a29 -r 302cfb533201 src/ODUtil.agda
--- a/src/ODUtil.agda	Sat May 20 09:48:37 2023 +0900
+++ b/src/ODUtil.agda	Sat May 20 18:28:22 2023 +0900
@@ -23,6 +23,7 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
+open ODAxiom-ho< odAxiom-ho<
 
 open HOD
 open _∧_
@@ -235,8 +236,10 @@
 ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso
 
 Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD }
+   →  {Ca : HOD} → {rca : RXCod A Ca ψa }
+   →  {Cb : HOD} → {rcb : RXCod B Cb ψb }
    → ( {z : Ordinal  } → (az : odef A z ) →  (ψa (* z) (subst (odef A) (sym &iso) az) ≡ ψb (* z) (subst (odef B) (sym &iso) (A⊆B az))))
-   → Replace' A ψa ⊆ Replace' B ψb
+   → Replace' A ψa rca ⊆ Replace' B ψb rcb
 Repl⊆ {A} {B} A⊆B {ψa} {ψb} eq  record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = A⊆B az
          ; x=ψz = trans  x=ψz (cong (&) (eq az) ) }
 
@@ -255,14 +258,15 @@
 
 -- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b
 -- ∋-irr {X} {x} _ _ = refl
---    is requed in
-Replace∩ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
-    → ( {x : HOD} → (a b : X ∋ x ) → ψ x a ≡ ψ x b )
-    → (Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))))   ⊆ ( Replace' P (λ _ p → ψ _ (P⊆X p)) ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q)))
-Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X ψ-irr = lem04 where
-    lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ))) x
-       → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p)) ∩ Replace' Q (λ z q → ψ z (Q⊆X q)))) x
-    lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪
-         record { z = _ ; az = proj1 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) }  ,
-         record { z = _ ; az = proj2 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) } ⟫
+--    is requireed in
+-- Replace∩ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
+--     →  {C : HOD} → (rc : RXCod X C ψ )
+--     → ( {x : HOD} → (a b : X ∋ x ) → ψ x a ≡ ψ x b )
+--     → Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))) {C} record { ≤COD = λ lt → RXCod.≤COD rc ?  }   ⊆ ( Replace' P (λ _ p → ψ _ (P⊆X p)) ? ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q)) ? )
+-- Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X rc ψ-irr = lem04 where
+--     lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ) ? )) x
+--        → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p) ) ?  ∩ Replace' Q (λ z q → ψ z (Q⊆X q)) ? )) x
+--     lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪
+--          record { z = _ ; az = proj1 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) }  ,
+--          record { z = _ ; az = proj2 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) } ⟫
 
diff -r 45cd80181a29 -r 302cfb533201 src/ZProduct.agda
--- a/src/ZProduct.agda	Sat May 20 09:48:37 2023 +0900
+++ b/src/ZProduct.agda	Sat May 20 18:28:22 2023 +0900
@@ -103,25 +103,28 @@
 ZFPair : OD
 ZFPair = record { def = λ x → ord-pair x }
 
-_⊗_ : (A B : HOD) → HOD
-A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
+-- _⊗_ : (A B : HOD) → HOD
+-- A ⊗ B  = Union ( Replace' B (λ b lb → Replace' A (λ a la → < a , b > ) record { ≤COD = ? } ) ? )
 
-product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
-product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2  } where
-    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
-    lemma1 = replacement← B b B∋b
-    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
-    lemma2 = replacement← A a A∋a
+-- product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+-- product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2  } where
+--     lemma1 :  odef (Replace' B (λ b₁ lb → Replace' A (λ a₁ la → < a₁ , b₁ >) ? ) ? ) (& (Replace' A (λ a₁ la → < a₁ , b >) ? ))
+--     lemma1 = ? -- replacement← B b B∋b ?
+--     lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >)
+--     lemma2 = ? -- replacement← A a A∋a ?
 
 data ZFProduct  (A B : HOD) : (p : Ordinal) → Set n where
     ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
 
 ZFP  : (A B : HOD) → HOD
 ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  }
-        ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) }
+        ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
    where
-        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x
-        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
+        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
+        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b
+        ... | tri< a<b ¬b ¬c = ?
+        ... | tri≈ ¬a a=b ¬c = ?
+        ... | tri> ¬a ¬b b<a = ?
 
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb )
@@ -150,22 +153,23 @@
 zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) ))
                               , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) )  ⟫
 
-ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
-ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
+-- ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
+-- ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
 
-⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
-⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
-       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
-       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
-       zfp01 : odef (ZFP A B) (& x)
-       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
-       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba)
+-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
+-- ⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
+--        zfp02 : Replace' A (λ z lz → < z , * a >) record { ≤COD = ? }  ≡ * owner
+--        zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
+--        zfp01 : odef (ZFP A B) (& x)
+--        zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
+--        ... | t = ?
+--        -- ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba)
 
 ZPI1 : (A B : HOD) → HOD
-ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px ))
+ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) ?
 
 ZPI2 : (A B  : HOD) → HOD
-ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px ))
+ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) ?
 
 ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
 ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
@@ -233,12 +237,12 @@
        is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
 
 data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
-     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > )))
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ) ? ))
 
 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
 FuncHOD→F {A} {B} (felm F) = F
 
-FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > )
+FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) ?
 FuncHOD=R {A} {B}  (felm F) = *iso
 
 --