--- 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 _ _)) } ⟫