Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1464:484f83b04b5d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Jan 2024 19:29:23 +0900
parents 9c19a7177b8a
children bd2b003e25ef
files src/BAlgebra.agda src/HODBase.agda src/OD.agda src/ODC.agda src/ODUtil.agda
diffstat 5 files changed, 193 insertions(+), 210 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/BAlgebra.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -1,118 +1,133 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
+{-# OPTIONS --cubical-compatible --safe #-}
 open import Level
 open import Ordinals
-module BAlgebra {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+module BAlgebra {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom )
+       (AC : OD.AxiomOfChoice O HODAxiom )
+   where
 
--- open import zf
+-- open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+open import Data.Unit
+open import Relation.Nullary
+open import Relation.Binary  hiding (_⇔_)
+open import Relation.Binary.Core hiding (_⇔_)
+import Relation.Binary.Reasoning.Setoid as EqR
+
 open import logic
 import OrdUtil
-import OD 
-import ODUtil
-import ODC
+open import nat
 
-open import Relation.Nullary
-open import Relation.Binary
-open import Data.Empty
-open import Relation.Binary
-open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
-
-open inOrdinal O
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
 -- open Ordinals.IsNext isNext
 open OrdUtil O
-open ODUtil O
+import ODUtil
+open ODUtil O HODAxiom ho<
+import ODC
 
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-open HOD
+-- Ordinal Definable Set
+
+open HODBase.HOD 
+open HODBase.OD 
 
 open _∧_
 open _∨_
 open Bool
 
-L＼L=0 : { L  : HOD  } → L ＼ L ≡ od∅ 
-L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← =  lem1 } ) where
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+open AxiomOfChoice AC
+
+open _∧_
+open _∨_
+open Bool
+
+L＼L=0 : { L  : HOD  } → (L ＼ L) =h= od∅ 
+L＼L=0 {L} = record { eq→ = lem0 ; eq← =  lem1 }  where
     lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
     lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
     lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
     lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
 
-L＼Lx=x : { L x : HOD  } → x ⊆ L   → L ＼ ( L ＼ x ) ≡ x
-L＼Lx=x {L} {x} x⊆L = ==→o≡ ( record { eq→ = lem03 ; eq← = lem04 } ) where
+L＼Lx=x : { L x : HOD  } → x ⊆ L   → (L ＼ ( L ＼ x )) =h= x
+L＼Lx=x {L} {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 }  where
     lem03 :  {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z 
-    lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O x (* z)
+    lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O HODAxiom AC  x (* z)
     ... | yes y = subst (λ k → odef x k ) &iso y 
     ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ )
     lem04 :  {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z 
-    lem04 {z} xz with ODC.∋-p O L (* z)
+    lem04 {z} xz with ODC.∋-p O HODAxiom AC L (* z)
     ... | yes y = ⟪ subst (λ k → odef L k ) &iso y  , ( λ p → proj2 p xz )  ⟫
     ... | no  n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) ))
      
-L＼0=L : { L  : HOD  } → L ＼ od∅ ≡ L 
-L＼0=L {L} = ==→o≡ ( record { eq→ = lem05 ; eq← = lem06 } ) where
+L＼0=L : { L  : HOD  } → (L ＼ od∅) =h= L 
+L＼0=L {L} = record { eq→ = lem05 ; eq← = lem06 }  where
     lem05 : {x : Ordinal} → odef (L ＼ od∅) x → odef L x
     lem05 {x} ⟪ Lx , _ ⟫ = Lx
     lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x
     lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt)  ⟫
 
 ∨L＼X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x
-∨L＼X {L} {X} {x} Lx with ODC.∋-p O X (* x)
+∨L＼X {L} {X} {x} Lx with ODC.∋-p O HODAxiom AC X (* x)
 ... | yes y = case1 ( subst (λ k → odef X k ) &iso y  )
 ... | no  n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫
 
 ＼-⊆ : { P A B : HOD } →  A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B ) 
 ＼-⊆ {P} {A} {B} A⊆P = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx  , (λ ax → proj2 pbx (a<b ax))   ⟫ )  , lem07 ⟫ where
     lem07 : (P ＼ B) ⊆ (P ＼ A) → A ⊆ B
-    lem07 pba {x} ax with ODC.p∨¬p O (odef B x)
+    lem07 pba {x} ax with ODC.p∨¬p O HODAxiom AC (odef B x)
     ... | case1 bx = bx
     ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax  , ¬bx ⟫ ) ax )
 
 RC＼ : {L : HOD} → RCod (Power (Union L)) (λ z → L ＼ z )
-RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz  } where
+RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz ; ψ-eq = λ {x} {y} → wdf {x} {y}  } where
     lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L )
     lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz }
+    wdf : {x y : HOD} → od x == od y → (L ＼ x) =h= (L ＼ y)
+    wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫ 
+                             ; eq← = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq→ x=y yp) ) ⟫  }
 
 
-[a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
-[a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+[a-b]∩b=0 : { A B : HOD } → ((A ＼ B) ∩ B) =h= od∅
+[a-b]∩b=0 {A} {B} = record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
      ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
 
 U-F=∅→F⊆U : {F U : HOD} →  ((x : Ordinal) →  ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
 U-F=∅→F⊆U {F} {U} not = gt02  where
     gt02 : { x : Ordinal } → odef F x → odef U x
-    gt02 {x} fx with ODC.∋-p O U (* x)
+    gt02 {x} fx with ODC.∋-p O HODAxiom AC U (* x)
     ... | yes y = subst (λ k → odef U k ) &iso y
     ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
 
-∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
-∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
+∪-Union : { A B : HOD } → Union (A , B) =h= ( A ∪ B )
+∪-Union {A} {B} = ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
-    lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo )
+    lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) ? (sym ?) abo )
     ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin 
          * owner ≡⟨ cong (*) (sym a=o)  ⟩ 
-         * (& A) ≡⟨ *iso ⟩ 
+         * (& A) ≡⟨ ? ⟩ 
          A ∎ ) ox ) where open ≡-Reasoning
-    ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox)
+    ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) ?  ) ox)
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) A
         ⟪ case1 refl , d→∋ A A∋x ⟫ )
     lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) B
         ⟪ case2 refl , d→∋ B B∋x ⟫ )
 
-∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
-∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )) ?  =h= ( A ∩ B )
+∩-Select {A} {B} =  record { eq→ =  lemma1 ; eq← = lemma2 }  where
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) ? ) x → odef (A ∩ B) x
     lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
-    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) ? ) x
     lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
 
-dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
-dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+dist-ord : {p q r : HOD } → (p ∩ ( q ∪ r )) =h=  ( ( p ∩ q ) ∪ ( p ∩ r ))
+dist-ord {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 }  where
     lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
     lemma1 {x} lt with proj2 lt
     lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ 
@@ -121,8 +136,8 @@
     lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ 
     lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ 
 
-dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
-dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+dist-ord2 : {p q r : HOD } → (p ∪ ( q ∩ r )) =h=  ( ( p ∪ q ) ∩ ( p ∪ r ))
+dist-ord2 {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 }  where
     lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
     lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
     lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
@@ -132,13 +147,13 @@
     lemma2 {x} lt | _ | case1 cp = case1 cp 
     lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
 
-record IsBooleanAlgebra {n : Level} ( L : Set n)
-       ( _==_ : L → L → Set n )
+record IsBooleanAlgebra {n m : Level} ( L : Set n)
+       ( _==_ : L → L → Set m )
        ( b1 : L )
        ( b0 : L )
        ( -_ : L → L  )
        ( _+_ : L → L → L )
-       ( _x_ : L → L → L ) : Set (suc n) where
+       ( _x_ : L → L → L ) : Set (n ⊔ m) where
    field
        +-assoc : {a b c : L } → (a + ( b + c )) == ((a + b) + c)
        x-assoc : {a b c : L } → (a x ( b x c )) == ((a x b) x c)
@@ -153,9 +168,9 @@
        a+-a1 : {a : L } → (a + ( - a )) == b1
        ax-a0 : {a : L } → (a x ( - a )) == b0
 
-record BooleanAlgebra {n : Level} ( L : Set n) : Set (suc n) where
+record BooleanAlgebra {n m : Level} ( L : Set n) : Set (n ⊔ suc m) where
    field
-       _=b=_ : L → L → Set n 
+       _=b=_ : L → L → Set m 
        b1 : L
        b0 : L
        -_ : L → L 
@@ -171,25 +186,25 @@
 
 open PowerP
 
-HODBA : (P : HOD) → BooleanAlgebra (PowerP P)
-HODBA P = record { _=b=_ = λ x y → hod x ≡ hod y ; b1 = ⟦ P , (λ x → x) ⟧   ; b0 = ⟦ od∅ , (λ x →  ⊥-elim (¬x<0 x)) ⟧ 
+HODBA : (P : HOD) → BooleanAlgebra {suc n} {n} (PowerP P)
+HODBA P = record { _=b=_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧   ; b0 = ⟦ od∅ , (λ x →  ⊥-elim (¬x<0 x)) ⟧ 
   ; -_ = λ x → ⟦  P ＼ hod x , proj1 ⟧
   ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧ 
    ; isBooleanAlgebra = record {
-       +-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = ba01 a b c ; eq← = ba02 a b c  }
-     ; x-assoc = λ {a} {b} {c} → ==→o≡ 
+       +-assoc = λ {a} {b} {c} →  record { eq→ = ba01 a b c ; eq← = ba02 a b c  }
+     ; x-assoc = λ {a} {b} {c} →  
         record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫ 
                ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ } 
-     ; +-sym = λ {a} {b} → ==→o≡ record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt  ; eq← = ba05 {hod b} {hod a} }
-     ; x-sym = λ {a} {b} → ==→o≡ record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
-     ; +-aab = λ {a} {b} → ==→o≡ record { eq→ = ba03 a b ; eq← = case1  }
-     ; x-aab = λ {a} {b} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax →  ⟪ ax , case1 ax ⟫ }
-     ; +-dist = dist-ord2
-     ; x-dist = dist-ord
-     ; a+0 = λ {a} → ==→o≡ record { eq→ = ba04 (hod a) ; eq← = case1 }
-     ; ax1 = λ {a} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ }
-     ; a+-a1 = λ {a} → ==→o≡ record { eq→ = ba06 a ; eq← = ba07 a }
-     ; ax-a0 =  λ {a} → ==→o≡ record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) }
+     ; +-sym = λ {a} {b} →  record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt  ; eq← = ba05 {hod b} {hod a} }
+     ; x-sym = λ {a} {b} →  record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
+     ; +-aab = λ {a} {b} →  record { eq→ = ba03 a b ; eq← = case1  }
+     ; x-aab = λ {a} {b} →  record { eq→ = proj1 ; eq← = λ ax →  ⟪ ax , case1 ax ⟫ }
+     ; +-dist = λ {p} {q} {r} → dist-ord2 {hod p} {hod q} {hod r} 
+     ; x-dist = λ {p} {q} {r} → dist-ord {hod p} {hod q} {hod r} 
+     ; a+0 = λ {a} →  record { eq→ = ba04 (hod a) ; eq← = case1 }
+     ; ax1 = λ {a} →  record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ }
+     ; a+-a1 = λ {a} →  record { eq→ = ba06 a ; eq← = ba07 a }
+     ; ax-a0 =  λ {a} →  record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) }
        } } where
      ba00 : (x y : PowerP P ) →  (hod x ∪ hod y) ⊆ P
      ba00 x y (case1 px) = x⊆P x px
@@ -205,7 +220,7 @@
      ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx)
      ba02 a b c {x} (case2 cx) = case2 (case2 cx)
      ba03 : (a b : PowerP P) → {x : Ordinal} →
-            odef (hod a) x ∨ odef (hod a ∩ hod b) x → OD.def (od (hod a)) x
+            odef (hod a) x ∨ odef (hod a ∩ hod b) x → def (od (hod a)) x
      ba03 a b (case1 ax) = ax
      ba03 a b (case2 ab) = proj1 ab
      ba04 : (a : HOD) →  {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x
@@ -214,13 +229,13 @@
      ba05 : {a b : HOD} {x : Ordinal} →  odef a x ∨ odef b x → odef b x ∨ odef a x
      ba05 (case1 x) = case2 x
      ba05 (case2 x) = case1 x
-     ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → OD.def (od P) x
+     ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → def (od P) x
      ba06 a {x} (case1 ax) = x⊆P a ax
      ba06 a {x} (case2 nax) = proj1 nax
-     ba07 : (a : PowerP P ) → { x : Ordinal} → OD.def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x 
-     ba07 a {x} px with ODC.∋-p O (hod a) (* x)
+     ba07 : (a : PowerP P ) → { x : Ordinal} → def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x 
+     ba07 a {x} px with ODC.∋-p O HODAxiom AC (hod a) (* x)
      ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y)
      ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫
-     ba08 : (a : PowerP P) → {x : Ordinal} → OD.def (od (hod a ∩ (P ＼ hod a))) x → OD.def (od od∅) x
+     ba08 : (a : PowerP P) → {x : Ordinal} → def (od (hod a ∩ (P ＼ hod a))) x → def (od od∅) x
      ba08 a {x} ⟪ ax , ⟪ px , nax ⟫ ⟫ = ⊥-elim ( nax ax )
 
--- a/src/HODBase.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/HODBase.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -100,3 +100,14 @@
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → (& x) ≡ (& y)
 
+==-Setoid : Setoid (suc n) n
+==-Setoid = record { _≈_ = λ x y → od x == od y ; Carrier = HOD 
+   ; isEquivalence = record { refl = ==-refl ; sym = ==-sym ; trans = ==-trans } }
+
+-- use as open 
+-- import Relation.Binary.EqReasoning as EqR
+-- open EqR ==-Setoid
+
+
+
+
--- a/src/OD.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/OD.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -43,6 +43,7 @@
 ==-trans = HODBase.==-trans O
 ==-sym = HODBase.==-sym O
 ⇔→== = HODBase.⇔→== O
+==-Setoid = HODBase.==-Setoid O
 
 -- possible order restriction (required in the axiom of Omega )
 
@@ -78,6 +79,16 @@
 _∋_ : ( a x : HOD  ) → Set n
 _∋_  a x  = odef a ( & x )
 
+                                                            
+record AxiomOfChoice : Set (suc n) where
+ field                      
+  -- mimimul and x∋minimal is an Axiom of choice                
+  minimal : (x : HOD  ) → ¬ (od x == od od∅ )→ HOD                                
+  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+  x∋minimal : (x : HOD  ) → ( ne : ¬ (od x == od od∅ ) ) → odef x ( & ( minimal x ne ) )
+  -- minimality (proved by ε-induction with LEM)
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (od x == od od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
+
 -- _c<_ : ( x a : HOD  ) → Set n
 -- x c< a = a ∋ x
 
@@ -118,6 +129,9 @@
 o≡→== : { x y : Ordinal  } → x ≡  y →  od (* x) == od (* y)
 o≡→==  {x} {.x} refl = ==-refl
 
+≡→== : { x y : HOD  } → x ≡  y →  od x == od y
+≡→==  {x} {.x} refl = ==-refl
+
 *≡*→≡ : { x y : Ordinal  } → * x ≡ * y →  x ≡ y
 *≡*→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) eq )
 
@@ -294,7 +308,7 @@
 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 
+     ψ-eq : ∀ {x y : HOD } → od x == od y  → ψ x =h= ψ y 
 
 record Replaced (A : HOD) (ψ : Ordinal → Ordinal ) (x : Ordinal ) : Set n where
    field
@@ -311,7 +325,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 (&) (RCod.ψ-eq rc *iso== ) }
+replacement← {ψ} X x lt {C} rc = record { z = & x ; az = lt  ; x=ψz = ==→o≡ (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)) 
--- a/src/ODC.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/ODC.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -1,47 +1,45 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 open import Level
 open import Ordinals
-module ODC {n : Level } (O : Ordinals {n} ) where
+import HODBase
+import OD
+module ODC {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) 
+       (AC : OD.AxiomOfChoice O HODAxiom )
+   where
 
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
-open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.Nat.Properties
 open import Data.Empty
+open import Data.Unit
 open import Relation.Nullary
-open import Relation.Binary
-open import Relation.Binary.Core
+open import Relation.Binary  hiding (_⇔_)
+open import Relation.Binary.Core hiding (_⇔_)
+import Relation.Binary.Reasoning.Setoid as EqR
 
+open import logic
 import OrdUtil
-open import logic
 open import nat
-import OD
-import ODUtil
-
-open inOrdinal O
-open OD O
-open OD.OD
-open OD._==_
-open ODAxiom odAxiom
-open ODUtil O
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
 -- open Ordinals.IsNext isNext
 open OrdUtil O
 
+-- Ordinal Definable Set
 
-open HOD
+open HODBase.HOD 
+open HODBase.OD 
 
 open _∧_
+open _∨_
+open Bool
 
-postulate
-  -- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD
-  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
-  -- minimality (proved by ε-induction with LEM)
-  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
+open  HODBase._==_
 
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+open AxiomOfChoice AC
 
 --
 -- Axiom of choice in intutionistic logic implies the exclude middle
@@ -60,15 +58,19 @@
 p∨¬p  p | yes eq = case2 (¬p eq) where
    ps = pred-od p
    eqo∅ : ps =h=  od∅  → & ps ≡  o∅
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
+   eqo∅ eq = trans (==→o≡ eq) ord-od∅
    lemma : ps =h= od∅ → p → ⊥
    lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
    ¬p : (& ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
+   ¬p eq =  lemma ( begin
+      pred-od p  ≈⟨ *iso== ⟩
+      * ( & ps ) ≡⟨ cong (*) eq ⟩
+      * ( o∅ ) ≈⟨ o∅==od∅ ⟩
+      od∅ ∎ ) where open EqR ==-Setoid
 p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
    ps = pred-od p
    eqo∅ : ps =h=  od∅  → & ps ≡  o∅
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
+   eqo∅ eq = trans (==→o≡ eq) ord-od∅
    lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq))
    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
 
@@ -99,18 +101,6 @@
 ... | case1 a = case1 a
 ... | case2 ¬a = case2 ( ab ¬a)
 
--- record By-contradiction (A : Set n) (B : A → Set n)  : Set (suc n) where
---  field
---     a : A
---     b : B a
--- 
--- by-contradiction : {A : Set n} {B : A → Set n}  → ¬ ( (a : A ) → ¬ B a ) → By-contradiction A B
--- by-contradiction {A} {B} not with p∨¬p A 
--- ... | case2 ¬a  = ⊥-elim (not (λ a → ⊥-elim (¬a a  )))
--- ... | case1 a with p∨¬p (B a)
--- ... | case1 b  = record { a = a ; b = b }
--- ... | case2 ¬b = ⊥-elim ( not ( λ a b → ⊥-elim ( ¬b ? )))
--- 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
 
@@ -133,12 +123,11 @@
     ; _∋_ = _∋_
     ; _≈_ = _=h=_
     ; ∅  = od∅
-    ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ 
     isZFC = record {
        choice-func = choice-func ;
        choice = choice
--- a/src/ODUtil.agda	Wed Jan 03 11:05:21 2024 +0900
+++ b/src/ODUtil.agda	Wed Jan 03 19:29:23 2024 +0900
@@ -13,6 +13,7 @@
 open import Relation.Nullary
 open import Relation.Binary  hiding (_⇔_)
 open import Relation.Binary.Core hiding (_⇔_)
+import Relation.Binary.Reasoning.Setoid as EqR
 
 open import logic
 import OrdUtil
@@ -35,24 +36,7 @@
 open  HODBase._==_
 
 open HODBase.ODAxiom HODAxiom  
-
--- HOD =  HODBase.HOD O 
--- OD  =  HODBase.OD O 
--- Ords  =  HODBase.Ords O 
--- _==_  =  HODBase._==_ O 
--- ==-refl = HODBase.==-refl  O
--- ==-trans = HODBase.==-trans O
--- ==-sym = HODBase.==-sym O
--- ⇔→== = HODBase.⇔→== O
-
 open OD O HODAxiom
--- open OD.OD
--- open ODAxiom odAxiom
--- open ODAxiom-ho< odAxiom-ho<
-
--- open HOD
--- open _∧_
--- open _==_
 
 _⊂_ : ( A B : HOD) → Set n
 _⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B )
@@ -136,9 +120,6 @@
 ω→nat : (n : HOD) → Omega ho< ∋ n → Nat
 ω→nat n = ω→nato
 
-ω→nat-cong : (n : HOD) → (x y : Omega ho< ∋ n) → ω→nat n x ≡ ω→nat n y
-ω→nat-cong n x y = ?
-
 ω∋nat→ω : {n : Nat} → def (od (Omega ho<)) (& (nat→ω n))
 ω∋nat→ω {Zero} = subst (λ k → def (od (Omega ho<)) k) (sym ord-od∅) iφ
 ω∋nat→ω {Suc n} =  subst (λ k → Omega-d k) (sym (==→o≡ nat01)) nat00 where
@@ -161,9 +142,6 @@
 single& (case1 eq) = sym (trans eq &iso)
 single& (case2 eq) = sym (trans eq &iso)
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
--- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
-
 pair=∨ : {a b c : Ordinal  } → odef (* a , * b) c → (  a ≡ c ) ∨  (  b ≡ c )
 pair=∨ {a} {b} {c} (case1 c=a) = case1 ( sym (trans c=a &iso))
 pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso))
@@ -183,83 +161,73 @@
         x ≡⟨ single& ( eq← *iso==  (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩
         y ∎ ) x<y)  where open ≡-Reasoning
 
-ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x
-ω-prev-eq {x} {y} eq with trio< x y
-ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
-ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = (sym b)
-ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
+Omega-inject : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x
+Omega-inject {x} {y} eq with trio< x y
+Omega-inject {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
+Omega-inject {x} {y} eq | tri≈ ¬a b ¬c = (sym b)
+Omega-inject {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
 
 ω-inject : {x y : HOD} →  Union ( y , ( y ,  y)) =h= Union ( x , ( x ,  x)) → y =h= x
-ω-inject {x} {y} eq = ord→== ( ω-prev-eq (==→o≡ (==-trans Omega-iso (==-trans eq (==-sym Omega-iso)))))
+ω-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≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
-ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
+ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) =h= od∅ )
+ωs≠0 x =  ∅< {Union ( x , ( x ,  x))} (ω-∈s  _)
+
+ω→nato-cong : {n m : Ordinal} → (x : odef (Omega ho< ) n) (y : odef (Omega ho< ) m) → n ≡ m → ω→nato x ≡ ω→nato y
+ω→nato-cong OD.iφ OD.iφ eq = refl
+ω→nato-cong OD.iφ (OD.isuc {x} y) eq = ⊥-elim ( ∅< {Union (* x , (* x , * x))} {* x} (ω-∈s _) (≡o∅→=od∅ (sym eq)   ) )
+ω→nato-cong (OD.isuc {x} y) OD.iφ eq = ⊥-elim ( ∅< {Union (* x , (* x , * x))} {* x} (ω-∈s _) (≡o∅→=od∅ eq   ) )
+ω→nato-cong (OD.isuc x) (OD.isuc y) eq = cong Suc ( ω→nato-cong x y (Omega-inject eq) )
 
 ωs0 : o∅ ≡ & (nat→ω 0)
 ωs0 = trans (sym ord-od∅) (cong (&) refl ) 
 
+Omega-subst : (x y : HOD) → x =h= y  →  Union ( x , (x , x)) =h= Union ( y , (y , y)) 
+Omega-subst x y x=y = begin
+    Union (x , (x , x)) ≈⟨ ==-sym Omega-iso ⟩ 
+    Union (* (& x) , (* (& x) , * (& x))) ≈⟨ ord→== (cong (λ k → & (Union (* k , (* k , * k )))) (==→o≡ x=y) )  ⟩ 
+    Union (* (& y) , (* (& y) , * (& y))) ≈⟨ Omega-iso ⟩ 
+    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 = ? where
-    nat→ω-iso-ord : (x : Ordinal) → odef (Omega ho< ) x → nat→ω ( ω→nat (* x) ? ) =h= (* x)
-    nat→ω-iso-ord x OD.iφ = ?
-    nat→ω-iso-ord x (OD.isuc lt) = ?
---     -- ε-induction {λ i →  Lift (suc n) ((lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i)  } ind i where
---     ind : {x : HOD} → ({y : HOD} → x ∋ y → Lift (suc n) ((lt : Omega ho< ∋ y) → nat→ω (ω→nat y lt) =h= y)) →
---                                            (Lift (suc n) ((lt : Omega ho< ∋ x) → nat→ω (ω→nat x lt) =h= x))
---     ind {x} prev = ? where
---         ind1 : {ox : Ordinal } → (ltd : Omega-d ox ) → * ox =h= x → nat→ω (ω→nato ltd) =h= x
---         ind1 {o∅} iφ eq = ==-sym ?
---         ind1 (isuc {x₁} ltd) ox=x = ? where
---         -- begin
---         --    nat→ω (ω→nato (isuc ltd) )
---         -- ≡⟨⟩
---         --    Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
---         -- ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
---         --    Union (* x₁ , (* x₁ , * x₁))
---         -- ≡⟨ trans ( sym ? ) ox=x ⟩
---         --    x
---         -- ∎ where
---               open ≡-Reasoning
---               lemma0 :  x ∋ * x₁
---               lemma0 = eq→  ox=x (eq→  *iso== 
---                   record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = eq→  *iso== (case1 refl)  })
---               lemma1 : Omega ho< ∋ * x₁
---               lemma1 = subst (λ k → odef (Omega ho<) k) (sym &iso) ltd
---               lemma3 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ? -- ltd ? ltd1
---               lemma3 = ?
---               -- lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
---               -- lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
---               -- lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (eq))
---               -- ... | t = ? -- HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq (sym eq))) t
---               lemma2 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
---               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
---                   lemma6 : {x y : Ordinal} → {ltd : Omega-d x } {ltd1 : Omega-d y } → y ≡ x → ? → ω→nato ltd ≡ ω→nato ltd1
---                   lemma6 = ? -- refl HE.refl = refl
---               lemma :  nat→ω (ω→nato ltd) =h= * x₁
---               lemma = ? -- trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → Omega-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
+nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) (==-sym *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.isuc {y} lt)) = ==-trans (Omega-subst _ _ 
+      (==-trans (Omega-subst _ _ lem02 ) *iso==) ) *iso==  where
+      lem02  : nat→ω ( ω→nato lt ) =h= (* y)
+      lem02  = nat→ω-iso-ord y lt
 
-
-ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : Omega-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x
+ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : Omega-d ox) → * ox =h= nat→ω x → ω→nato ltd ≡ x
 ω→nat-iso0 Zero iφ eq = refl
-ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) ? ))
-ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅  ) ? eq ))
+ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (begin
+    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 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where
-       lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
-       lemma1 eq = subst (λ k → * x ≡ k ) ? (cong (λ k → * k)
-            (sym ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
-                (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym ? ) eq )))))))
+       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)))) ≈⟨  eq ⟩
+             Union ((nat→ω i) , (nat→ω i , nat→ω i)) ≈⟨ ==-sym Omega-iso ⟩
+             Union (* (& (nat→ω i)) , (* (& (nat→ω i)) , * (& (nat→ω i)))) ∎ )) ))  ⟩
+          * (& ( nat→ω i))  ≈⟨ (==-sym *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}) ?
+ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) (==-sym *iso==)
 
-nat→ω-inject : {i j : Nat} → nat→ω i ≡  nat→ω j → i ≡ j
+nat→ω-inject : {i j : Nat} → nat→ω i =h=  nat→ω j → i ≡ j
 nat→ω-inject {Zero} {Zero} eq = refl
-nat→ω-inject {Zero} {Suc j} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) eq)) refl ))
-nat→ω-inject {Suc i} {Zero} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) (sym eq))) refl ))
-nat→ω-inject {Suc i} {Suc j} eq = ? -- cong Suc (nat→ω-inject {i} {j} ( ω-inject ? ))
+nat→ω-inject {Zero} {Suc j} eq = ⊥-elim ( ∅< {Union (nat→ω j , (nat→ω j , nat→ω j))} (ω-∈s  _) (==-sym eq) )
+nat→ω-inject {Suc i} {Zero} eq = ⊥-elim ( ∅< {Union (nat→ω i , (nat→ω i , nat→ω i))} (ω-∈s  _) eq )
+nat→ω-inject {Suc i} {Suc j} eq = cong Suc (nat→ω-inject {i} {j} ( ω-inject eq ))
 
 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 }
@@ -282,17 +250,3 @@
     lem03 :   odef (* (& P)) (& (p ∩ q))
     lem03 = eq→  *iso== ( each (ppx _ xz) (ppy _ yz) )
 
--- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b
--- ∋-irr {X} {x} _ _ = refl
---    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 _ _)) } ⟫
-