--- a/src/ODUtil.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/ODUtil.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -50,6 +50,17 @@
 ⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c
 ⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab)
 
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x))  where
+   t1 : {x : HOD }  → t ∋ x → A ∋ x
+   t1 = power→ A t PA∋t
+
+power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
+power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01  where
+   p01 :  {z : HOD} → (x ∩ y) ∋ z → A ∋ z
+   p01 {z} xyz = power→ A x ax (proj1 xyz )
+
+
 cseq :  HOD  →  HOD
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
@@ -148,7 +159,7 @@
 
 ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
 ω-prev-eq1 {x} {y} eq x<y with  eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl
-        ; ox = eq→ *iso== (case1 refl) }   --  (* x , (* x , * x)) ∋ * y
+        ; ox = eq→ (==-sym *iso) (case1 refl) }   --  (* x , (* x , * x)) ∋ * y
 ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u
 ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin
        osuc y ≡⟨ sym (cong osuc  &iso) ⟩
@@ -158,7 +169,7 @@
        & (* x) ≡⟨ &iso ⟩
        x ∎ ))) where open o≤-Reasoning O
 ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin
-        x ≡⟨ single& ( eq← *iso==  (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩
+        x ≡⟨ single& ( eq← (==-sym *iso)  (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩
         y ∎ ) x<y)  where open ≡-Reasoning
 
 Omega-inject : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x
@@ -171,7 +182,7 @@
 ω-inject {x} {y} eq = ord→== ( Omega-inject (==→o≡ (==-trans Omega-iso (==-trans eq (==-sym Omega-iso)))))
 
 ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
-ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl  ; ox = eq→ *iso== (case2 refl) }
+ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl  ; ox = eq→ (==-sym *iso) (case2 refl) }
 
 ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) =h= od∅ )
 ωs≠0 x =  ∅< {Union ( x , ( x ,  x))} (ω-∈s  _)
@@ -193,12 +204,12 @@
     Union (y , (y , y)) ∎ where open EqR ==-Setoid                       
 
 nat→ω-iso : {i : HOD} → (lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i
-nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) (==-sym *iso==) where
+nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) *iso where
     nat→ω-iso-ord : (x : Ordinal) → (lt : odef (Omega ho< ) x) → nat→ω ( ω→nato lt ) =h= (* x)
     nat→ω-iso-ord _ OD.iφ = ==-sym o∅==od∅
-    nat→ω-iso-ord x (OD.isuc OD.iφ) = ==-trans (Omega-subst _ _ (==-sym o∅==od∅)) *iso==
+    nat→ω-iso-ord x (OD.isuc OD.iφ) = ==-trans (Omega-subst _ _ (==-sym o∅==od∅)) (==-sym *iso)
     nat→ω-iso-ord x (OD.isuc (OD.isuc {y} lt)) = ==-trans (Omega-subst _ _ 
-      (==-trans (Omega-subst _ _ lem02 ) *iso==) ) *iso==  where
+      (==-trans (Omega-subst _ _ lem02 ) (==-sym *iso)))  (==-sym *iso)  where
       lem02  : nat→ω ( ω→nato lt ) =h= (* y)
       lem02  = nat→ω-iso-ord y lt
 
@@ -208,20 +219,20 @@
     Union (nat→ω x , (nat→ω x , nat→ω x)) ≈⟨ ==-sym eq ⟩
     * o∅ ≈⟨ o∅==od∅  ⟩
     od∅ ∎ )) where open EqR ==-Setoid
-ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (==-trans *iso== eq) )
+ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (==-trans (==-sym *iso) eq) )
 ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where
        lemma1 :  * (& (Union (* x , (* x , * x)))) =h= Union (nat→ω i , (nat→ω i , nat→ω i)) → * x =h= nat→ω i
        lemma1 eq = begin
           * x  ≈⟨ (o≡→== ( Omega-inject  (==→o≡ (begin
-             Union (* x , (* x , * x)) ≈⟨  *iso== ⟩
+             Union (* x , (* x , * x)) ≈⟨ ==-sym  *iso ⟩
              * (& ( Union (* x , (* x , * x)))) ≈⟨  eq ⟩
              Union ((nat→ω i) , (nat→ω i , nat→ω i)) ≈⟨ ==-sym Omega-iso ⟩
              Union (* (& (nat→ω i)) , (* (& (nat→ω i)) , * (& (nat→ω i)))) ∎ )) ))  ⟩
-          * (& ( nat→ω i))  ≈⟨ (==-sym *iso==)  ⟩
+          * (& ( nat→ω i))  ≈⟨ *iso ⟩
           nat→ω i ∎  where open EqR ==-Setoid
 
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) (==-sym *iso==)
+ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso
 
 nat→ω-inject : {i j : Nat} → nat→ω i =h=  nat→ω j → i ≡ j
 nat→ω-inject {Zero} {Zero} eq = refl
@@ -238,7 +249,7 @@
          ; x=ψz = trans  x=ψz (cong (&) (eq az) ) }
 
 PPP : {P : HOD} → Power P ∋ P
-PPP {P} z pz = eq← *iso== pz
+PPP {P} z pz = eq← (==-sym *iso) pz
 
 UPower⊆Q : {P Q : HOD} → P ⊆ Q → Union (Power P) ⊆ Q
 UPower⊆Q {P} {Q} P⊆Q {z} record { owner = y ; ao = ppy ; ox = yz } = P⊆Q (ppy _ yz)
@@ -248,5 +259,5 @@
 UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz }
    =  record { owner = & P ; ao = PPP ; ox = lem03 }  where
     lem03 :   odef (* (& P)) (& (p ∩ q))
-    lem03 = eq→  *iso== ( each (ppx _ xz) (ppy _ yz) )
+    lem03 = eq→  (==-sym *iso) ( each (ppx _ xz) (ppy _ yz) )