# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688105309 -32400
# Node ID 4b72bc3e2fab86fea6e4e19b226a117a81c41b3f
# Parent  e5192c07777fb5def0c5e1834489e1543e1fb977
...

diff -r e5192c07777f -r 4b72bc3e2fab src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 12:22:26 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 15:08:29 2023 +0900
@@ -135,27 +135,19 @@
       gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
          ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } 
 
-      data gfImage : (i : ℕ) (x : Ordinal) → Set n where
-          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
-          next-gf : {x : Ordinal} → {i : ℕ} → (ix : IsImage a a gf x) → (gfiy : gfImage i (IsImage.y ix) ) → gfImage (suc i) x
-
-      a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
-      a∋gfImage 0 {x} (a-g ax ¬ib) = ax
-      a∋gfImage (suc i) {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt ) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
+      data gfImage :  (x : Ordinal) → Set n where
+          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage  x
+          next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage.y ix) ) → gfImage  x
 
-      C : ℕ → HOD                                               --  Image {& (C i)} {a} (gf i)  does not work
-      C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } 
-
-      record CN (x : Ordinal) : Set n where
-          field 
-             i : ℕ
-             gfix : gfImage i x
+      a∋gfImage : {x : Ordinal } → gfImage x → odef (* a) x
+      a∋gfImage {x} (a-g ax ¬ib) = ax
+      a∋gfImage  {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt ) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
 
       UC : HOD
-      UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
+      UC = record { od = record { def = λ x → gfImage x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage lt)  }
 
       a-UC : HOD
-      a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ CN x) } ; odmax = & (* a) 
+      a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ gfImage x) } ; odmax = & (* a) 
           ; <odmax = λ lt → odef< (proj1 lt)  }
       
       --  UC ⊆ * a
@@ -163,8 +155,8 @@
       --     g : Image f UC → UC    is injection
 
       UC⊆a : * (& UC) ⊆ * a
-      UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02)  where
-            be02 : CN x
+      UC⊆a {x} lt = a∋gfImage  be02  where
+            be02 : gfImage x
             be02 = subst (λ k → odef k x) *iso lt
 
       a-UC⊆a : * (& a-UC) ⊆ * a
@@ -178,27 +170,27 @@
       fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → fba x bx ≡ fba y bx1
       fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
 
-      UC∋gf : {y : Ordinal } → (uy : odef (* (& UC)) y ) → CN ( fba (fab y (UC⊆a uy) ) (b∋fab y  (UC⊆a uy)))
-      UC∋gf {y} uy = record { i = suc (CN.i uc00) ; gfix = next-gf record { y = _ ; ay = UC⊆a uy ; x=fy = fba-eq (fab-eq refl) }  (CN.gfix uc00) } where
-          uc00 : CN y
+      UC∋gf : {y : Ordinal } → (uy : odef (* (& UC)) y ) → gfImage ( fba (fab y (UC⊆a uy) ) (b∋fab y  (UC⊆a uy)))
+      UC∋gf {y} uy = next-gf record { y = _ ; ay = UC⊆a uy ; x=fy = fba-eq (fab-eq refl) }  uc00  where
+          uc00 : gfImage y
           uc00 = subst (λ k → odef k y) *iso uy
 
-      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → ¬ odef (C 0) x → Ordinal
-      g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
+      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ (¬ IsImage b a g x) ) → Ordinal
+      g⁻¹ {x} ax nc0  with ODC.p∨¬p O ( IsImage b a g x )
       ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = y
-      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism  )
 
-      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x) → odef (* b) (g⁻¹ ax nc0)
+      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : ¬ (¬ IsImage b a g x )) → odef (* b) (g⁻¹ ax nc0)
       b∋g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
       ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ay
-      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism )
 
-      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
+      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ (¬ IsImage b a g x )) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
       g⁻¹-iso {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
       ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
-      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism )
 
-      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : ¬ odef (C 0) (fba x bx) ) → g⁻¹ (a∋fba x bx) nc0  ≡ x
+      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : ¬ (¬ IsImage b a g (fba x bx) ))  → g⁻¹ (a∋fba x bx) nc0  ≡ x
       g⁻¹-iso1 {x} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) 
 
       be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x
@@ -206,9 +198,9 @@
           be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
           be15 {x} lt with subst (λ k → odef k x) *iso lt
           ... | ⟪ ax , ncn ⟫ = ax
-          be16 : {x : Ordinal } → odef (* (& a-UC)) x → ¬ odef (C 0) x
+          be16 : {x : Ordinal } → odef (* (& a-UC)) x →  ¬ ( ¬ IsImage b a g x )  
           be16 {x} lt nc0 with subst (λ k → odef k x) *iso lt
-          ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn record { i = 0 ; gfix = nc0 } )
+          ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn ? )
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
           be17 x lt = subst ( λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) (sym *iso) ⟪ be19 , 
                  (λ img → be18 be14 (subst (λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) *iso img) )  ⟫  where
@@ -217,7 +209,7 @@
               be19 : odef (* b) (g⁻¹ (be15 lt) (be16 lt))
               be19 = b∋g⁻¹ (be15 lt) (be16 lt)
               be18 : odef a-UC x →  ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 lt) (be16 lt))
-              be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → CN k) be13 (UC∋gf ay) ) where
+              be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be13 (UC∋gf ay) ) where
                    be13 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x
                    be13 = begin
                       fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy)  ⟩
@@ -234,18 +226,18 @@
           be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be15 ⟫ where
               be16 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)
               be16 = proj2 ( subst (λ k → odef k x) (*iso) lt )
-              be15 : ¬ CN (be13 x lt)
-              be15 cn with CN.i cn | CN.gfix  cn
-              ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } )
-              ... | suc i | next-gf  record { y = y ; ay = ay ; x=fy = x=fy } t 
+              be15 : ¬ gfImage (be13 x lt)
+              be15 cn with cn
+              ... | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } )
+              ... | next-gf  record { y = y ; ay = ay ; x=fy = x=fy } t 
                    = ⊥-elim (be16 (subst (λ k → odef k x) (sym *iso) record { y = y 
-                      ; ay = subst (λ k → odef k y) (sym *iso) record { i = i ; gfix = t } ; x=fy = be17 })) where
-                  be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) (record { i = i ; gfix = t })))
+                      ; ay = subst (λ k → odef k y) (sym *iso) t ; x=fy = be17 })) where
+                  be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) t))
                   be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl)
      
       a-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& a-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx)  ≡ x
       a-UC-iso0 x cx = trans (fba-eq refl) ( g⁻¹-iso (proj1 ( subst (λ k → odef k x) (*iso) cx )) 
-         (λ cn → ⊥-elim (proj2 ( subst (λ k → odef k x) (*iso) cx ) record { i = 0 ; gfix = cn} ) ))
+         (λ cn → ⊥-elim ? ))
 
       a-UC-iso1 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
       a-UC-iso1 x cx with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) )
@@ -255,12 +247,12 @@
       --   C n → f (C n) 
       fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
       fU x lt = be03 where
-            be02 : CN x
+            be02 : gfImage x
             be02 = subst (λ k → odef k x) *iso lt
             be03 : Ordinal
-            be03 with CN.i be02 | CN.gfix be02
-            ... | zero | a-g {x} ax ¬ib = fab x ax
-            ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
+            be03 with be02
+            ... | a-g {x} ax ¬ib = fab x ax
+            ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
                    = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) ))
 
       --   f (C n) → g (f (C n) ) ≡ C (suc i)
@@ -270,23 +262,23 @@
 
       be04 : {x : Ordinal } →  (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx)
       be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where
-            be02 : CN x
+            be02 : gfImage x
             be02 = subst (λ k → odef k x) *iso cx
             be06 :  odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx)
-            be06 with CN.i be02 | CN.gfix be02
-            ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
-            ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
+            be06 with be02
+            ... | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
+            ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
                 = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
 
       UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx)  ≡ x
       UC-iso0 x cx = be03 where
-            be02 : CN x
+            be02 : gfImage x
             be02 = subst (λ k → odef k x) *iso cx
             be03 : Uf ( fU x cx ) (be04 cx)  ≡ x
-            be03 with CN.i be02 | CN.gfix be02 | be04 cx
-            ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect  (fU x) cx
+            be03 with be02 | be04 cx
+            ... | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect  (fU x) cx
             ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _  ax (UC⊆a ay) x=fy )
-            be03 | suc i | next-gf record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | cb with 
+            be03 | next-gf record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | cb with 
                       subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1))))  ) *iso cb 
             ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _  ax (UC⊆a ay) x=fy ) where
                   ax : odef (* a) x
@@ -300,14 +292,14 @@
       UC-iso1 x cx = be14 where
             be14 : fU ( Uf x cx ) (be08 cx)  ≡ x
             be14 with subst (λ k → odef k x) *iso cx
-            ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay)
-            ... | 0 | a-g ax ¬ib = sym x=fy
-            ... | (suc i) | next-gf t ix = sym x=fy
+            ... | record { y = y ; ay = ay ; x=fy = x=fy } with subst (λ k → OD.def (od k) y) *iso ay
+            ... | a-g ax ¬ib = sym x=fy
+            ... | next-gf t ix = sym x=fy
 
       h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal
       h {x} ax with ODC.∋-p O UC (* x)
-      ... | yes cn  = fU x (subst (λ k → odef k x ) (sym *iso) (subst (λ k → CN k) &iso cn) )
-      ... | no ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , subst (λ k → ¬ (CN k)) &iso ncn ⟫ )
+      ... | yes cn  = fU x (subst (λ k → odef k x ) (sym *iso) (subst (λ k → gfImage k) &iso cn) )
+      ... | no ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , subst (λ k → ¬ (gfImage k)) &iso ncn ⟫ )
 
       h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal
       h⁻¹ {x} bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
@@ -318,10 +310,10 @@
 
       be70 : (x : Ordinal) (lt : odef (* a) x) → odef (* b) (h lt)
       be70 x ax = ? 
-      -- with ODC.p∨¬p O ( CN x )
+      -- with ODC.p∨¬p O ( gfImage x )
       --... | case1 cn  = be03 (subst (λ k → odef k x) (sym *iso) cn) where    -- make the same condition for Uf
       --     be03 : (cn : odef (* (& UC)) x) → odef (* b) (fU x cn )
-      --     be03 cn with CN.i (subst (λ k → odef k x) *iso cn) | CN.gfix (subst (λ k → odef k x) *iso cn )
+      --     be03 cn with gfImage.i (subst (λ k → odef k x) *iso cn) | gfImage.gfix (subst (λ k → odef k x) *iso cn )
       --     ... | zero | a-g ax ¬ib = b∋fab x ax
       --     ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = b∋fab x
       --           (subst (odef (* a)) (sym x=fy) (a∋fba (fab y ay) (b∋fab y ay)))
@@ -366,7 +358,7 @@
 
            be75 : h (be71 x bx) ≡ x
            be75 with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)
-           ... | case1 cn  = trans ? (be78 (be73 cn)) where
+           ... | case1 cn  = ? where --  trans ? (be78 (be73 cn)) where
                 be78 : (auf : odef (* a) (Uf x (subst (λ k → odef k x) (sym *iso) cn))) → h auf ≡ x
                 be78 = ?
            ... | case2 ncn = ?