# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719051836 -32400
# Node ID d0b4be1cab0d66fda14643cf77bc022f22b57f52
# Parent  e970149a6af54772483551e3e3f57669e0714f58
...

diff -r e970149a6af5 -r d0b4be1cab0d src/ZProduct.agda
--- a/src/ZProduct.agda	Sat Jun 22 12:39:58 2024 +0900
+++ b/src/ZProduct.agda	Sat Jun 22 19:23:56 2024 +0900
@@ -424,10 +424,9 @@
 
 record Injection (A B : Ordinal ) : Set n where
    field
-       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
-       irr : (x : Ordinal ) → ( lt1 lt2 : odef (* A)  x ) → i→ x lt1 ≡ i→ x lt2 
-       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
-       inject : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
+       i→  : (x : Ordinal ) → Ordinal
+       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x  )
+       inject : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ≡ i→ y → x ≡ y
 
 record HODBijection (A B : HOD ) : Set n where
    field
diff -r e970149a6af5 -r d0b4be1cab0d src/bijection.agda
--- a/src/bijection.agda	Sat Jun 22 12:39:58 2024 +0900
+++ b/src/bijection.agda	Sat Jun 22 19:23:56 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module bijection where
 
@@ -47,8 +47,8 @@
 bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y
 bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso←  rs _) (fiso← rs _) (cong (fun← rs) eq)
 
-bi-∨  : {n m n1 m1 : Level } {A : Set n} {B : Set m} {C : Set n1} {D : Set m1}  → (ab : Bijection A B) → (cd : Bijection C D ) 
-       → Bijection (A ∨ C) (B ∨ D)           
+bi-∨  : {n m n1 m1 : Level } {A : Set n} {B : Set m} {C : Set n1} {D : Set m1}  → (ab : Bijection A B) → (cd : Bijection C D )
+       → Bijection (A ∨ C) (B ∨ D)
 bi-∨  {_} {_} {_} {_} {A} {B} {C} {D} ab cd = record {
          fun→  = fun→1
        ; fun←  = fun←1
@@ -64,7 +64,7 @@
     fiso→1 : (x : B ∨ D) → fun→1 (fun←1 x) ≡ x
     fiso→1 (case1 a) = cong case1 (fiso→ ab a)
     fiso→1 (case2 c) = cong case2 (fiso→ cd c)
-    fiso←1 : (x : A ∨ C) → fun←1 (fun→1 x) ≡ x 
+    fiso←1 : (x : A ∨ C) → fun←1 (fun→1 x) ≡ x
     fiso←1 (case1 a) = cong case1 (fiso← ab a)
     fiso←1 (case2 c) = cong case2 (fiso← cd c)
 
@@ -238,8 +238,8 @@
      --
      nn zero = record { j = 0 ; k = 0 ; k1 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
-     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i)
-     ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0
+     nn (suc i) with NN.k (nn i)  in eq
+     ... | zero = record { k = suc (sum ) ; j = 0
          ; k1 = nn02 ; nn-unique = nn04 } where
             ---
             --- increment the stage
@@ -283,7 +283,7 @@
                   i ∎   where open ≡-Reasoning
                nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
                nn06 = NN.nn-unique (nn i)
-     ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ;  nn-unique = nn13 } where
+     ... | suc k  = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ;  nn-unique = nn13 } where
             ---
             --- increment in a stage
             ---
@@ -459,8 +459,8 @@
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
          lb05 x eq = lb=b [] x (sym eq)
-     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n)
-     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
+     lb (suc n) with LB.nlist (lb n) in eq
+     ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
          open ≡-Reasoning
          lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
          lb10 = begin
@@ -471,7 +471,7 @@
            suc n ∎
          lb06 :  (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
          lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
-     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
+     ... | false ∷ t =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩
@@ -482,7 +482,7 @@
            suc n ∎  where open ≡-Reasoning
         lb09 :  (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
         lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) --  lton (true ∷ t) ≡ lton x
-     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
+     ... | true ∷ t = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
         lb03 : lton (true ∷ t) ≡ n
         lb03 = begin
            lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩
@@ -535,55 +535,55 @@
 record IsImage0 (A B : Set ) (f : (x : A ) → B) (x : B ) : Set  where
    field
       y : A
-      x=fy : x ≡ f y 
+      x=fy : x ≡ f y
 
-IsImage : (a b : Set) (iab : InjectiveF a b ) (x : b ) → Set 
+IsImage : (a b : Set) (iab : InjectiveF a b ) (x : b ) → Set
 IsImage a b iab x = IsImage0 a b (InjectiveF.f iab) x
 
-Bernstein : (A B : Set) 
-     → (fi : InjectiveF A  B ) → (gi : InjectiveF  B A )
-     → (is-A : (b : B ) → Dec (Is A B (InjectiveF.f fi) b)  )
-     → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a)  )
-     → Bijection A B
-Bernstein A B fi gi isa isb = ?  where
-    open InjectiveF
-    gfi : InjectiveF A A
-    gfi = record { f = λ x → f gi (f fi x) ; inject = λ {x} {y} eq → inject fi (inject gi eq) }
-    data gfImage :  (x : A) → Set where
-       a-g : {x : A} → (¬ib : ¬ ( IsImage B A gi x )) → gfImage  x
-       next-gf : {x : A} → (ix : IsImage A A gfi x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage  x
-    data ¬gfImage :  (x : A) → Set where
-       ngf : {x : A} → (¬gfiy : ¬ gfImage x) → ¬gfImage  x
-    gf02 : {x : A} → IsImage B A gi x ∨ (¬ IsImage B A gi x) ∨ ((ix : IsImage A A gfi x) →  ¬  gfImage (IsImage0.y ix)  ) → ¬ gfImage x
-    gf02 {x} c gf = ?
-    gfi∨ : (x : A) → gfImage x ∨ ¬gfImage x
-    gfi∨ x with isb x
-    ... | no ¬ib = case1 ( a-g (λ ib → ¬ib (record { a = IsImage0.y ib ; fa=c = sym (IsImage0.x=fy ib) })))
-    ... | yes ib with isa (f fi x)
-    ... | no ¬ia = case2 ( ngf ? )
-    ... | yes ia = case1 ( next-gf record { y = f gi (Is.a ib) ; x=fy = br00 }  (a-g br01 ) ) where
-         br00 :  x ≡ f gi (f fi (f gi (Is.a ib)))
-         br00 = ?
-         br01 :  ¬ IsImage B A gi (f gi (Is.a ib))
-         br01 record { y = y ; x=fy = x=fy } = ?
+--   Bernstein : (A B : Set)
+--        → (fi : InjectiveF A  B ) → (gi : InjectiveF  B A )
+--        → (is-A : (b : B ) → Dec (Is A B (InjectiveF.f fi) b)  )
+--        → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a)  )
+--        → Bijection A B
+--   Bernstein A B fi gi isa isb = ?  where
+--       open InjectiveF
+--       gfi : InjectiveF A A
+--       gfi = record { f = λ x → f gi (f fi x) ; inject = λ {x} {y} eq → inject fi (inject gi eq) }
+--       data gfImage :  (x : A) → Set where
+--          a-g : {x : A} → (¬ib : ¬ ( IsImage B A gi x )) → gfImage  x
+--          next-gf : {x : A} → (ix : IsImage A A gfi x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage  x
+--       data ¬gfImage :  (x : A) → Set where
+--          ngf : {x : A} → (¬gfiy : ¬ gfImage x) → ¬gfImage  x
+--       gf02 : {x : A} → IsImage B A gi x ∨ (¬ IsImage B A gi x) ∨ ((ix : IsImage A A gfi x) →  ¬  gfImage (IsImage0.y ix)  ) → ¬ gfImage x
+--       gf02 {x} c gf = ?
+--       gfi∨ : (x : A) → gfImage x ∨ ¬gfImage x
+--       gfi∨ x with isb x
+--       ... | no ¬ib = case1 ( a-g (λ ib → ¬ib (record { a = IsImage0.y ib ; fa=c = sym (IsImage0.x=fy ib) })))
+--       ... | yes ib with isa (f fi x)
+--       ... | no ¬ia = case2 ( ngf ? )
+--       ... | yes ia = case1 ( next-gf record { y = f gi (Is.a ib) ; x=fy = br00 }  (a-g br01 ) ) where
+--            br00 :  x ≡ f gi (f fi (f gi (Is.a ib)))
+--            br00 = ?
+--            br01 :  ¬ IsImage B A gi (f gi (Is.a ib))
+--            br01 record { y = y ; x=fy = x=fy } = ?
 
 
 Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
      → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )
-     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) 
+     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c ))
      → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
      → Bijection B ℕ
 Countable-Bernstein A B C an cn fi gi is-A is-B = record {
        fun→  = λ x → bton x
      ; fun←  = λ n → ntob n
      ; fiso→ = biso
-     ; fiso← = biso1 
+     ; fiso← = biso1
    } where
     --
     --     an     f     g     cn
     --   ℕ ↔   A  →  B  →  C  ↔   ℕ
     --            B = Image A f ∪ (B \ Image A f )
-    -- 
+    --
     open Bijection
     f = InjectiveF.f fi
     g = InjectiveF.f gi
@@ -646,7 +646,7 @@
     c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j
     c-mono i j i≤j with ≤-∨ i≤j
     ... | case1 refl = ≤-refl
-    c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) 
+    c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j)
     c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j)
 
     inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
@@ -693,7 +693,7 @@
         lem02 zero (h ∷ t) refl with is-A (fun← cn zero)
         ... | yes _ = refl
         ... | no _ = refl
-        lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) 
+        lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n))
         ... | yes _ = cong suc (lem02 n t refl)
         ... | no _ = lem02 n t refl
 
@@ -705,7 +705,7 @@
 
     --  count of a in a-list is one step reduced
     --
-    a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
+    a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )
         → suc (ca-list (a-list i cl a)) ≡ ca-list cl
     a-list-ca i cl a = lem03 i cl _ a refl where
          lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  → cal ≡  (a-list i cl a) → suc (ca-list cal)  ≡ ca-list cl
@@ -721,13 +721,13 @@
 
     --  reduced list still have all ani j < i
     --
-    a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
-         → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) 
+    a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )
+         → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a)
     a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where
-         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  
-             → cal ≡  (a-list i cl a) 
+         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )
+             → cal ≡  (a-list i cl a)
              → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) cal
-         lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< 
+         lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡<
              (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i )
          lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b
          lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px)
@@ -745,14 +745,14 @@
          --
 
          del : (i : ℕ) → (cl : List C) → any-cl i cl → List C   -- del 0 contains ani 0
-         del i cl a = a-list i cl (a i ≤-refl)  
+         del i cl a = a-list i cl (a i ≤-refl)
          del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del (suc i) cl a )
          del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where
-            lem41 : (cl dl : List C) 
+            lem41 : (cl dl : List C)
                  → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl)
-                 → (aj : Any (_≡_ (g (f (fun← an j)))) cl) 
+                 → (aj : Any (_≡_ (g (f (fun← an j)))) cl)
                  → dl ≡ a-list (suc i) cl ai →   Any (_≡_ (g (f (fun← an j)))) dl
-            lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< 
+            lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡<
                  (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) )
             lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k →  Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0
             lem41 (h ∷ t) y (there a0) (here px) refl = here px
@@ -760,17 +760,17 @@
 
          del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl  )
               → suc (ca-list (del i cl a)) ≡ ca-list cl
-         del-ca i cl a = a-list-ca i cl (a i ≤-refl) 
+         del-ca i cl a = a-list-ca i cl (a i ≤-refl)
 
          lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl
          lem30 0 cl i≤n a = begin
-             1 ≤⟨ s≤s z≤n ⟩ 
+             1 ≤⟨ s≤s z≤n ⟩
              suc (ca-list (del 0 cl a) )  ≡⟨ del-ca 0 cl a ⟩
              ca-list cl ∎ where
                 open ≤-Reasoning
          lem30 (suc i) cl i≤n a = begin
-            suc (suc i)   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 
-            suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
+            suc (suc i)   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩
+            suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩
             ca-list cl ∎ where
                 open ≤-Reasoning
 
@@ -814,14 +814,14 @@
         lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j
         lem06 i j bi bj eq = lem08  where
             lem20 : (i j : ℕ) → i < j →  Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥
-            lem20 zero (suc j) i<j bi bj le with  is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j)
-            ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
-            ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
-            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
+            lem20 zero (suc j) i<j bi bj le with  is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2
+            ... | no nisc  | _ = ⊥-elim (nisc bi)
+            ... |  yes _ |  no nisc = ⊥-elim (nisc bj)
+            ... | yes _ |  yes _  = ⊥-elim ( nat-≤> lem25 a<sa) where
                  lem22 : 1 ≡ count-B 0
-                 lem22 with is-B (fun← cn 0) | inspect count-B 0
-                 ... | yes _ | record { eq = eq1 } = refl
-                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem22 with is-B (fun← cn 0) in eq1
+                 ... | yes _ = refl
+                 ... | no nisa = ⊥-elim ( nisa bi )
                  lem24 : count-B j ≡ 0
                  lem24 = cong pred le
                  lem25 : 1 ≤ 0
@@ -837,18 +837,18 @@
                  --    cb i <  suc (cb i) < cb (suc i) ≤ cb j
                  --    suc (cb i) ≡ suc (cb j) → cb i ≡ cb j
                  lem22 : suc (count-B i) ≡ count-B (suc i)
-                 lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-                 ... | yes _ | record { eq = eq1 } = refl
-                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem22 with is-B (fun← cn (suc i)) in eq1
+                 ... | yes _ = refl
+                 ... | no nisa = ⊥-elim ( nisa bi )
                  lem23 : suc (count-B j) ≡ count-B (suc j)
-                 lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j)
-                 ... | yes _ | record { eq = eq1 } = refl
-                 ... | no nisa | _ = ⊥-elim ( nisa bj )
+                 lem23 with is-B (fun← cn (suc j)) in eq1
+                 ... | yes _ = refl
+                 ... | no nisa = ⊥-elim ( nisa bj )
                  lem24 : count-B i ≡ count-B j
-                 lem24 with  is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j)
-                 ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
-                 ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
-                 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le)
+                 lem24 with  is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2
+                 ... | no nisc  | _ = ⊥-elim (nisc bi)
+                 ... |  yes _ | no nisc  = ⊥-elim (nisc bj)
+                 ... | yes _ | yes _ = sym (cong pred le)
                  lem21 : suc (count-B i) ≤ count-B j
                  lem21 = begin
                      suc (count-B i) ≡⟨ lem22 ⟩
@@ -861,33 +861,46 @@
             ... | tri≈ ¬a b ¬c = b
             ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
 
+
         lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
-        lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 
-                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+        lem07 n 0 eq with is-B (fun← cn 0)
+        ... | yes isb = lem13 where
+            cb1 = count-B 0
+            lem14 : count-B 0 ≡ 1
+            lem14 with  is-B (fun← cn 0)
+            ... | yes _ = refl
+            ... | no ne = ⊥-elim (ne isb)
             lem12 : (cb1 : ℕ) →  Is B C g (fun← cn cb1)  → 1 ≡ count-B cb1 → 0 ≡ cb1
-            lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) 
-        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
-        lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
-                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq)
+            lem13 : CountB n
+            lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
+                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq)   }
+        ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+        lem07 n (suc i) eq with is-B (fun← cn (suc i))
+        ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq
+                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq)   } where
+            cbs = count-B (suc i)
+            lem14 : count-B (suc i) ≡ suc (count-B i)
+            lem14 with  is-B (fun← cn (suc i))
+            ... | yes _ = refl
+            ... | no ne = ⊥-elim (ne isb)
             lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
-            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq)
-        ... | no nisb | record { eq = eq1 } = lem07 n i  eq
+            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq)
+        ... | no nisb = lem07 n i eq
 
         -- starting from 0, if count B i ≡ suc n, this is it
 
         lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
         lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
         ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
-        ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
-        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
+        ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1
+        ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+        ... | no nisb = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
         lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
         ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
-        ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
-        ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+        ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1
+        ... | yes isb = lem09 i j lt (cong pred eq)
+        ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq
 
     bton : B → ℕ
     bton b = pred (count-B (fun→ cn (g b)))
@@ -896,7 +909,7 @@
     ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
-    biso n = begin  
+    biso n = begin
         bton (ntob n) ≡⟨ refl ⟩
         pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩
         pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩
@@ -910,18 +923,18 @@
     -- uniqueness of ntob is proved by injection
     --
     biso1 : (b : B) → ntob (bton b) ≡ b
-    biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) 
-    ... | zero  | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
+    biso1 b with count-B (fun→ cn (g b)) in eq1
+    ... | zero  = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
         lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero
         lem20 = eq1
         lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B  i
-        lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = ≤-refl
-        ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
-        lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record{ eq = eq2 } = s≤s z≤n
-        ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
-    ... | suc n | record { eq = eq1 } = begin 
+        lem21 0 eq with is-B (fun← cn 0) in eq1
+        ... | yes isb = ≤-refl
+        ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+        lem21 (suc i) eq with is-B (fun← cn (suc i)) in eq1
+        ... | yes isb = s≤s z≤n
+        ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+    ... | suc n = begin
            CountB.b CB  ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin
               fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩
               fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩
@@ -1031,7 +1044,7 @@
    ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
    ... | no n = no lem00 where
         lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫
-        lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } 
+        lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl }
    dec1 ⟪ h ∷ t , false ∷ bt ⟫  with dec1 ⟪ h ∷ t , bt ⟫
    ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) }
    ... | no n = no lem00 where
@@ -1051,7 +1064,7 @@
 --   just true ∷ just true ∷ nothing ∷ just true ∷ just true ∷ nothing ∷      just true ∷ nothing ∷ []
 --
 -- LBBℕ : Bijection (List (List Bool)) ℕ
---          
+--
 -- Lℕ=ℕ : Bijection (List ℕ) ℕ
 --
 
diff -r e970149a6af5 -r d0b4be1cab0d src/cardinal.agda
--- a/src/cardinal.agda	Sat Jun 22 12:39:58 2024 +0900
+++ b/src/cardinal.agda	Sat Jun 22 19:23:56 2024 +0900
@@ -1,44 +1,71 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
 
-open import Level hiding (suc ; zero )
+open import Level
 open import Ordinals
-module cardinal {n : Level } (O : Ordinals {n}) where
+import HODBase
+import OD
+open import Relation.Nullary
+module cardinal {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom )
+       (AC : OD.AxiomOfChoice O HODAxiom ) where
+
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 open import logic
--- import OD
-import OD 
-
-import ODC
-open import Data.Nat 
-open import Relation.Binary.PropositionalEquality
-open import Data.Nat.Properties
-open import Data.Empty
-open import Relation.Nullary
-open import Relation.Binary
-open import Relation.Binary.Core
+open import nat
 
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-open import ZProduct O
-
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
--- open Ordinals.IsNext isNext
 open OrdUtil O
-open ODUtil O
-
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+open ODUtil O HODAxiom  ho<
 
 open _∧_
 open _∨_
 open Bool
-open _==_
+
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+open import Level
+open import Ordinals
+
+import filter 
 
-open HOD
+open import Relation.Nullary 
+-- open import Relation.Binary hiding ( _⇔_ )
+open import Data.Empty 
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+import BAlgebra 
+
+-- open BAlgebra O
+open import ZProduct O HODAxiom ho<
+
+
+-------
+--    the set of finite partial functions from ω to 2
+--
+--
+
+open import Data.List hiding (filter)
+open import Data.Maybe 
+
 
 -- record HODBijection (A B : HOD ) : Set n where
 --   field
@@ -49,7 +76,7 @@
 --       fiso→ : (x : Ordinal ) → ( lt : odef A  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
 --       fiso← : (x : Ordinal ) → ( lt : odef B  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
  
-open Injection
+open Injection        -- in ZProduct
 open HODBijection
 
 record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where
@@ -59,7 +86,7 @@
       x=fy : x ≡ f y ay
 
 IsImage : (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) → Set n 
-IsImage a b iab x = IsImage0 (* a) (* b) (i→ iab) x
+IsImage a b iab x = IsImage0 (* a) (* b) (λ x ax → i→ iab x) x
 
 Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD
 Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
@@ -78,23 +105,37 @@
 
 open import BAlgebra O
 
-_-_ : (a b : Ordinal ) → Ordinal 
-a - b = & ( (* a) ＼ (* b) )
-
--→<  : (a b : Ordinal ) → (a - b) o≤ a
--→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) )
-
-b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x
-b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt
-... | ⟪ bx , ¬ax ⟫ = bx
+b-a⊆b : {a b x : Ordinal } → odef ((* b) ＼ (* a)) x → odef (* b) x
+b-a⊆b {a} {b} {x} ⟪ bx , nax ⟫ = bx
 
 Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
-Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx) 
-        ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq  } 
+Injection-⊆ {a} {b} {c} le f = record { i→ = λ x → i→ f x  ; iB = λ x cx → iB f x (le cx) 
+        ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq  }
 
 Injection-∙ : {a b c : Ordinal } → Injection a b → Injection b c → Injection a c
-Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax)
-        ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq)   } 
+Injection-∙ {a} {b} {c} f g = record { i→ = λ x  → i→ g (i→ f x ) ; iB = λ x ax → iB g (i→ f x ) (iB f x ax) 
+           ; inject = λ x y ix iy eq → inject f _ _ ix iy (inject g _ _ (iB f x ix ) (iB f y iy ) eq ) }
+
+==-bi : {A B C : HOD } → (ab : HODBijection A B) 
+    → ( (x : Ordinal ) → ( lt1 lt2 : odef A  x ) → fun→ ab x lt1 ≡ fun→ ab x lt2 )
+    → ( (x : Ordinal ) → ( lt1 lt2 : odef B  x ) → fun← ab x lt1 ≡ fun← ab x lt2 )
+    → (A =h= C → HODBijection C B) ∧ (B =h= C → HODBijection A C) 
+proj1 (==-bi {A} {B} {C} ab wld→ wld← ) a=c = record {
+         fun→  = λ x cx → fun→ ab x (eq← a=c cx)
+       ; fun←  = λ x bx → fun← ab x bx
+       ; funB  = λ x cx → funB ab x (eq← a=c cx)
+       ; funA  = λ x cx → eq→ a=c (funA ab x cx)
+       ; fiso→ = λ x bx → trans (wld→ _ _ _) (fiso→ ab x bx)
+       ; fiso← = λ x cx → fiso← ab x (eq← a=c cx)
+       } 
+proj2 (==-bi {A} {B} {C} ab wld→ wld←) b=c = record {
+         fun→  = λ x cx → fun→ ab x cx
+       ; fun←  = λ x bx → fun← ab x (eq← b=c bx)
+       ; funB  = λ x cx → eq→  b=c (funB ab x cx)
+       ; funA  = λ x cx → funA ab x (eq← b=c cx)
+       ; fiso→ = λ x cx → fiso→ ab x (eq← b=c cx)
+       ; fiso← = λ x bx → trans (wld← _ _ _) (fiso← ab x bx)
+       }    
 
 --
 -- Two injection can be joined
@@ -139,10 +180,10 @@
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b)
 Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) 
                   ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject })
-     = subst₂ (λ j k → HODBijection j k ) (sym a=UC∨a-UC) (sym b=fUC∨b-fUC) (bi-∪  bi-UC  bi-fUC)
+     = proj1 (==-bi (proj2 (==-bi (bi-∪  bi-UC  bi-fUC) ? ? ) (==-sym b=fUC∨b-fUC)) ? ? ) (==-sym a=UC∨a-UC) 
  where
       gf : Injection a a
-      gf = record { i→ = λ x ax → g (f x ax) (b∋f x ax) ; iB = λ x ax → a∋g _ (b∋f x ax) 
+      gf = record { i→ = λ x → g (f x ) ; iB = λ x ax → a∋g _ (b∋f x ax) 
          ; inject = λ x y ax ay eq → f-inject _ _ ax ay ( g-inject _ _ (b∋f _ ax) (b∋f _ ay) eq) } 
 
       -- HOD UC is closure of gi ∙ fi starting from a - Image g
@@ -179,18 +220,21 @@
       a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ gfImage x) } ; odmax = & (* a) 
           ; <odmax = λ lt → odef< (proj1 lt)  }
 
-      a=UC∨a-UC : * a ≡ UC ∪ a-UC
-      a=UC∨a-UC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where
+      a=UC∨a-UC : (* a) =h= (UC ∪ a-UC)
+      a=UC∨a-UC = record { eq→ = be00 ; eq← = be01 } where
            be00 : {x : Ordinal} → odef (* a) x → odef (UC ∪ a-UC) x
-           be00 {x} ax with ODC.p∨¬p O ( gfImage x)
+           be00 {x} ax with p∨¬p ( gfImage x)
            ... | case1 gfx = case1 gfx
            ... | case2 ngfx = case2 ⟪ ax , ngfx ⟫
            be01 : {x : Ordinal} → odef (UC ∪ a-UC) x → odef (* a) x 
            be01 {x} (case1 gfx) = a∋gfImage gfx
            be01 {x} (case2 ngfx) = proj1 ngfx
 
+      wld-a : (x : Ordinal) (lt1 lt2 : odef (UC ∪ a-UC) x) → ? -- fa bi-UC bi-fUC x lt1 ≡ fa bi-UC bi-fUC x lt2
+      wld-a = ?
+
       FA : (x : Ordinal) → (ax : gfImage x) → Ordinal
-      FA x ax = f x (a∋gfImage ax)
+      FA x ax = f x -- (a∋gfImage ax)
 
       b∋f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x
       b∋f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋f y (a∋gfImage ay))
@@ -201,10 +245,10 @@
       b-fUC : HOD
       b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA  x) } ; odmax = & (* b) ; <odmax = λ lt → odef∧< lt  }
 
-      b=fUC∨b-fUC : * b ≡ fUC ∪ b-fUC
-      b=fUC∨b-fUC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where
+      b=fUC∨b-fUC : * b =h= (fUC ∪ b-fUC)
+      b=fUC∨b-fUC = record { eq→ = be00 ; eq← = be01 } where
            be00 : {x : Ordinal} → odef (* b) x → odef (fUC ∪ b-fUC) x
-           be00 {x} bx with ODC.p∨¬p O (IsImage0 UC (* b) FA  x)
+           be00 {x} bx with p∨¬p  (IsImage0 UC (* b) FA  x)
            ... | case1 gfx = case1 gfx
            ... | case2 ngfx = case2 ⟪ bx , ngfx ⟫
            be01 : {x : Ordinal} → odef (fUC ∪ b-fUC) x → odef (* b) x 
@@ -212,15 +256,15 @@
            be01 {x} (case2 ngfx) = proj1 ngfx
 
       nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a gi x
-      nimg {x} ax ncn with ODC.p∨¬p O (IsImage b a gi x)
+      nimg {x} ax ncn with p∨¬p  (IsImage b a gi x)
       ... | case1 img = img
       ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
 
-      f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ax ≡ f y ax1
-      f-cong {x} {x} {ax} {ax1} refl = cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
+      f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ≡ f y 
+      f-cong {x} {x} {ax} {ax1} refl = ? -- cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
 
-      g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x bx ≡ g y bx1
-      g-cong {x} {x} {bx} {bx1} refl = cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
+      g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x ≡ g y 
+      g-cong {x} {x} {bx} {bx1} refl = ? -- cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
 
       g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → Ordinal
       g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y
@@ -228,10 +272,10 @@
       b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : IsImage b a gi x ) → odef (* b) (g⁻¹ ax nc0)
       b∋g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
-      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → g (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
+      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → g (g⁻¹ ax nc0)  ≡ x
       g⁻¹-iso {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
-      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a gi (g x bx) )  → g⁻¹ (a∋g x bx) nc0  ≡ x
+      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a gi (g x ) )  → g⁻¹ (a∋g x bx) nc0  ≡ x
       g⁻¹-iso1 {x} bx nc0 = inject gi _ _ (b∋g⁻¹ (a∋g x bx) nc0) bx (g⁻¹-iso (a∋g x bx) nc0) 
 
       g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a gi x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0'
@@ -240,25 +284,25 @@
 
       cc11-case2 : {x : Ordinal} (ax : odef (* a) x) 
           → (ncn : ¬ gfImage x) 
-          → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax))  (g⁻¹ ax (nimg ax ncn))
+          → ¬ IsImage0 UC (* b) (λ x ax → f x )  (g⁻¹ ax (nimg ax ncn))
       cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } with nimg ax ncn
       ... | record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } = ncn ( subst (λ k → gfImage k) be113 
                                             (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) )  where
-               be113 : g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡ x
+               be113 : g (f y )  ≡ x
                be113 = begin
-                    g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡⟨ g-cong (sym x=fy)  ⟩
-                    g y1 ay1 ≡⟨ sym (x=fy1) ⟩
+                    g (f y )  ≡⟨ g-cong (sym x=fy)  ⟩
+                    g y1 ≡⟨ sym (x=fy1) ⟩
                     x ∎ where open ≡-Reasoning
 
       cc10-case2 : {x : Ordinal } → (bx : odef (* b) x )
-         → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax))  x
-         → ¬ gfImage (g x bx)
+         → ¬ IsImage0 UC (* b) (λ x ax → f x )  x
+         → ¬ gfImage (g x )
       cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl }
       cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) 
            = nix record { y = _ ; ay = gfy ; x=fy = inject gi _ _ bx (b∋f y (a∋gfImage gfy)) (trans x=fy (g-cong (f-cong refl))) }
 
       fU1 : (x : Ordinal) → odef UC x → Ordinal
-      fU1 x gfx = f x (a∋gfImage gfx)
+      fU1 x gfx = f x 
 
       f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
       f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = y
@@ -277,7 +321,7 @@
 
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
-         fun→  = λ x lt → f x (a∋gfImage lt)
+         fun→  = λ x lt → f x 
        ; fun←  = λ x lt → f⁻¹ x lt
        ; funB  = λ x lt → record { y = _ ; ay = lt  ; x=fy = refl }
        ; funA  = λ x lt → UC∋f⁻¹ lt
@@ -288,21 +332,21 @@
       b-FUC∋g⁻¹ : {x : Ordinal } → (lt : odef a-UC x )→ odef b-fUC (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) 
       b-FUC∋g⁻¹ {x} ⟪ ax , ngfix ⟫ = ⟪ b∋g⁻¹ ax (nimg ax ngfix) , cc11-case2 ax ngfix  ⟫
 
-      a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (g x (proj1 lt ))
+      a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (g x )
       a-UC∋g {x} ⟪ bx , ¬img ⟫ = ⟪ a∋g x bx , cc10-case2 bx ¬img ⟫
 
       fUC-iso1 : {x : Ordinal } → (lt : odef b-fUC x ) → g⁻¹ (proj1 (a-UC∋g lt)) (nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))) ≡ x
       fUC-iso1 {x} lt with nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))
       ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject gi _ _ (proj1 lt) ay x=fy )
 
-      fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) →  g (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) (proj1 (b-FUC∋g⁻¹ lt)) ≡ x
+      fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) →  g (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt)))  ≡ x
       fUC-iso0 {x} lt with nimg (proj1 lt) (proj2 lt)
       ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
       bi-fUC : HODBijection a-UC b-fUC
       bi-fUC = record { 
          fun→  = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))
-       ; fun←  = λ x lt → g x (proj1 lt)
+       ; fun←  = λ x lt → g x 
        ; funB  = λ x lt → b-FUC∋g⁻¹  lt
        ; funA  = λ x lt → a-UC∋g lt
        ; fiso→ = λ x lt → fUC-iso1 lt
@@ -326,17 +370,17 @@
 -- Cardinal⊆ = {!!}                                              -- we may have infinite sets with the same cardinality
 
 PtoF : {u : HOD} {x s : Ordinal } → odef (Power u) s → odef u x → Bool
-PtoF {u} {x} {s} su ux with ODC.p∨¬p O (odef (* s) x )
+PtoF {u} {x} {s} su ux with p∨¬p (odef (* s) x )
 ... | case1 a = true
 ... | case2 b = false
 
 fun←cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  
     → x ≡ y  → fun← b x ax ≡ fun← b y ax1
-fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
+fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
      
 fun→cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef P x} {ax1 : odef P y}  
     → x ≡ y  → fun→ b x ax ≡ fun→ b y ax1
-fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 ))  
+fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 ))  
      
 
 --    S
@@ -347,29 +391,29 @@
 Cantor1 : ( S : HOD ) → S c< Power S
 Cantor1 S f = diag4 where 
      f1 : Injection (& S) (& (Power S))
-     f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = c02 }where
+     f1 = record { i→ = λ x → & (* x , * x) ; iB = c00 ;  inject = c02 }where
          c02 : (x y : Ordinal) (ltx : odef (* (& S)) x) (lty : odef (* (& S)) y) →
             & (* x , * x) ≡ & (* y , * y) → x ≡ y
-         c02 x y ltx lty eq = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (xx=zy→x=y c03 )) where
+         c02 x y ltx lty eq = ? where -- subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (xx=zy→x=y c03 )) where
              c03 : (* x , * x) =h= (* y , * y)
              c03 = ord→== eq
          c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
-         c00 x lt = subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z  )) where
+         c00 x lt = ? where -- subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z  )) where
              c01 : (y : Ordinal ) → odef (* x , * x ) y  → odef S y
-             c01 y (case1 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
-             c01 y (case2 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
+             c01 y (case1 eq) = ? --- subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
+             c01 y (case2 eq) = ? -- subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
      f2 : Injection (& (Power S)) (& S) 
      f2 = f
-     postulate   -- yes we have a proof but it is very slow
-         b : HODBijection (Power S) S 
-     -- b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)   -- this makes check very slow
+     -- postulate   -- yes we have a proof but it is very slow
+     b : HODBijection (Power S) S 
+     b = subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1)   -- this makes check very slow
      --      but postulate makes check weak eg. irrerevance of ∋ 
 
      -- we have at least one element since Power S contains od∅
      --
 
      p0 : odef (Power S) o∅
-     p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
+     p0 z xz = ? -- ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
 
      s : Ordinal 
      s = fun→ b o∅ p0
@@ -378,7 +422,7 @@
      ss = funB b o∅ p0
 
      is-S : (S : HOD) → (x : Ordinal ) →  Bool
-     is-S S x with ODC.p∨¬p O (odef S x )
+     is-S S x with p∨¬p (odef S x )
      ... | case1 _ = true
      ... | case2 _ = false
 
@@ -390,21 +434,21 @@
          ; odmax = & S ; <odmax = odef∧< } 
 
      diag3 : odef (Power S) (& Diag)
-     diag3 z xz with subst (λ k → odef k z) *iso xz
-     ... | ⟪ sx , eq ⟫ = sx
+     diag3 z xz = ? -- with subst (λ k → odef k z) *iso xz
+     -- ... | ⟪ sx , eq ⟫ = sx
 
      not-isD : (x : Ordinal) → (sn : odef S x)  → not (  is-S (* (fun← b x sn )) x ) ≡ is-S Diag x
-     not-isD x sn with  ODC.p∨¬p O (odef (* (fun← b x sn )) x)  | ODC.p∨¬p O (odef Diag x) | inspect (is-S (* (fun← b x sn ))) x
-     ... | case1 lt | case1 ⟪ sx , eq ⟫ | record { eq = eq1 } = ⊥-elim (¬t=f false (trans (sym eq1) (eq sn )) )
-     ... | case1 lt | case2 lt1 | _ = refl
-     ... | case2 lt | case1 lt1 | _ = refl
-     ... | case2 lt | case2 neg | record { eq = eq1 } = ⊥-elim ( neg ⟪ sn , (λ sx → trans (cong diag ( HE.≅-to-≡ ( ∋-irr {S} sx sn ))) eq1 ) ⟫ )
+     not-isD x sn with  p∨¬p (odef (* (fun← b x sn )) x)  | p∨¬p (odef Diag x) | (is-S (* (fun← b x sn ))) x in eq1
+     ... | case1 lt | case1 ⟪ sx , eq ⟫ | _ = ? -- ⊥-elim (¬t=f false (trans (sym eq1) (eq sn )) )
+     ... | case1 lt | case2 lt1 | _ = ?
+     ... | case2 lt | case1 lt1 | _ = ? -- refl
+     ... | case2 lt | case2 neg | _ = ? --⊥-elim ( neg ⟪ sn , (λ sx → trans (cong diag ( HE.≅-to-≡ ( ∋-irr {S} sx sn ))) eq1 ) ⟫ )
 
 
      diagn1 : (n : Ordinal ) → odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n)
      diagn1 n sn dn = ¬t=f (is-S Diag n) (begin
           not (is-S Diag n)
-        ≡⟨ cong (λ k → not (is-S k n)) (sym *iso) ⟩
+        ≡⟨ cong (λ k → not (is-S k n)) (sym ? ) ⟩
           not (is-S (* (& Diag)) n)
         ≡⟨ cong (λ k → not (is-S (* k) n)) (sym (fiso← b (& Diag) diag3 )) ⟩
           not (  is-S (* (fun← b (fun→ b (& Diag) diag3) (funB b (& Diag) diag3 ))) n ) 
@@ -419,11 +463,11 @@
      diag4 = diagn1  (fun→ b (& Diag) diag3) (funB b (& Diag) diag3) refl
  
 c<¬= : { u s : HOD } →  u c< s → ¬ ( u =c=  s )
-c<¬= {u} {s} c<u ceq = c<u record { i→ = λ x lt → fun← ceq x (subst (λ k → odef k x) *iso lt) 
-     ; iB = λ x lt → subst₂ (λ j k → odef j k) (sym *iso) refl (funA ceq x (subst (λ k → odef k x) *iso lt))  
+c<¬= {u} {s} c<u ceq = c<u record { i→ = λ x  → fun← ceq x (subst (λ k → odef k x) ? ?) 
+     ; iB = λ x lt → subst₂ (λ j k → odef j k) (sym ?) refl (funA ceq x (subst (λ k → odef k x) ? lt))  
      ; inject = c04 } where
          c04 :  (x y : Ordinal) (ltx : odef (* (& (s))) x) (lty : odef (* (& (s))) y) 
-            → fun← ceq x (subst (λ k → odef k x) *iso ltx) ≡ fun← ceq y (subst (λ k → odef k y) *iso lty) → x ≡ y
+            → fun← ceq x (subst (λ k → odef k x) ? ltx) ≡ fun← ceq y (subst (λ k → odef k y) ? lty) → x ≡ y
          c04 x y ltx lty eq = begin
            x ≡⟨ sym ( fiso→ ceq x c05 ) ⟩
            fun→ ceq ( fun← ceq x c05 ) (funA ceq x c05)  ≡⟨ fun←cong (hodbij-sym ceq) eq ⟩
@@ -431,9 +475,9 @@
            y ∎ where 
              open ≡-Reasoning
              c05 : odef (s) x
-             c05 = subst (λ k → odef k x) *iso ltx
+             c05 = subst (λ k → odef k x) ? ltx
              c06 : odef (s) y
-             c06 = subst (λ k → odef k y) *iso lty
+             c06 = subst (λ k → odef k y) ? lty
 
 Cantor2 : (u : HOD) → ¬ ( u =c=  Power u )
 Cantor2 u =  c<¬= (Cantor1 u )
diff -r e970149a6af5 -r d0b4be1cab0d src/partfunc.agda
--- a/src/partfunc.agda	Sat Jun 22 12:39:58 2024 +0900
+++ b/src/partfunc.agda	Sat Jun 22 19:23:56 2024 +0900
@@ -1,33 +1,72 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
+
 open import Level
-open import Relation.Nullary 
-open import Relation.Binary.PropositionalEquality
--- open import Ordinals
-module partfunc {n : Level } where -- (O : Ordinals {n})  where
+open import Ordinals
+import HODBase
+import OD
+open import Relation.Nullary
+module partfunc {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom ) where
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 open import logic
-open import Relation.Binary 
-open import Data.Empty 
-open import Data.Unit using ( ⊤ ; tt )
-open import Data.List hiding (filter)
-open import Data.Maybe  
-open import Relation.Binary
-open import Relation.Binary.Core
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
--- open import filter O
+open import nat
+
+open OrdUtil O
+open ODUtil O HODAxiom  ho<
 
 open _∧_
 open _∨_
 open Bool
 
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+
+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⊔_ )
+
+open import Data.Empty 
+open import Data.Unit using ( ⊤ ; tt )
+open import Data.List hiding (filter ; find)
+open import Data.Maybe  
+
+open _∧_
+open _∨_
+open Bool
+
+data Two : Set where
+  i0 : Two
+  i1 : Two
+
 ----
 --
 -- Partial Function without ZF
 --
 
-record PFunc  (Dom : Set n) (Cod : Set n) : Set (suc n) where
+record PFunc {n m l : Level } (Dom : Set n) (Cod : Set m) : Set (suc  (n ⊔ m ⊔ l)) where
    field
-      dom : Dom → Set n
+      dom : Dom → Set l
       pmap : (x : Dom ) → dom x → Cod
       meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
 
@@ -36,26 +75,26 @@
 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
 --
 
-data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where
-   v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v  ∷ f ) Zero
-   vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) 
+data Findp {n : Level} {Cod : Set n} : List (Maybe Cod) → (x : Nat) → Set (suc n) where
+   v0 : {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v  ∷ f ) Zero
+   vn : {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) 
 
 open PFunc
 
-find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
+find : {n : Level} {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
 find (just v ∷ _) 0 (v0 v) = v
 find (_ ∷ n) (Suc i) (vn p) = find n i p
 
-findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
+findpeq : {n : Level} {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
 findpeq n {0} {v0 _} {v0 _} = refl
 findpeq [] {Suc x} {()}
 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
 
-List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
-List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x))
+List→PFunc : {Cod : Set (suc n)} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
+List→PFunc fp = record { dom = λ x → Lift zero (Findp fp (lower x))
                        ; pmap = λ x y → find fp (lower x) (lower y)
-                       ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} 
+                       ; meq = λ {x} {p} {q} →  findpeq fp {lower x} {lower p} {lower q}
                        }
 ----
 --