--- a/src/ODUtil.agda	Mon Jan 16 22:43:09 2023 +0900
+++ b/src/ODUtil.agda	Tue Jan 17 11:21:18 2023 +0900
@@ -46,6 +46,22 @@
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
     lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
 
+∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
+∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ =  λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
+
+_∪_ : ( A B : HOD  ) → HOD
+A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
+    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
+      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
+      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
+      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
+
+_＼_ : ( A B : HOD  ) → HOD
+A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
+
+¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
+¬∅∋ {x} = ¬x<0
+
 
 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
 pair-xx<xy {x} {y} = ⊆→o≤  lemma where
@@ -231,3 +247,26 @@
    =  record { owner = & P ; ao = PPP ; ox = lem03 }  where
     lem03 :   odef (* (& P)) (& (p ∩ q))
     lem03 = subst (λ k → odef k (& (p ∩ q))) (sym *iso) ( each (ppx _ xz) (ppy _ yz) )
+
+-- ∋-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 )
+--     → 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 = ==→o≡ record { eq→ = lem04 ; eq← = ? } 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 = ? }  ,
+--          record { z = _ ; az = proj2 az ; x=ψz = ? } ⟫
+
+Repl∪ψ : {X P Q : HOD}  → (ψ : (x : HOD) → X ∋ x → HOD) → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) → (x : HOD) → (P ∪ Q) ∋ x → HOD
+Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case1 p) = ψ _ (P⊆X p)
+Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case2 q) = ψ _ (Q⊆X q)
+
+Replace∪ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
+    → Replace' (P ∪ Q) (Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∪ Replace' Q (λ _ q → ψ _ (Q⊆X q))
+Replace∪ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = ? ; eq← = ? }
+
+
+