# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688002910 -32400
# Node ID 6dc3eb544387c5398dfcab03c4a1c1e863863cbc
# Parent  5476e93726e308cc2e70f6fb94254cfa35ef2e3e
a-UC

diff -r 5476e93726e3 -r 6dc3eb544387 src/cardinal.agda
--- a/src/cardinal.agda	Thu Jun 29 10:01:29 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 10:41:50 2023 +0900
@@ -154,8 +154,9 @@
       UC : HOD
       UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
 
-      b-UC : HOD
-      b-UC = record { od = record { def = λ x → (bx : odef (* b) x) →  ¬ CN (fba x bx) } ; odmax = & (* b) ; <odmax = λ lt → ? } -- odef< (proj1 lt)  }
+      a-UC : HOD
+      a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ CN x) } ; odmax = & (* a) 
+          ; <odmax = λ lt → odef< (proj1 lt)  }
       
       --  UC ⊆ * a
       --     f : UC → Image f UC    is injection
@@ -166,8 +167,8 @@
             be02 : CN x
             be02 = subst (λ k → odef k x) *iso lt
 
-      b-UC⊆b : * (& b-UC) ⊆ * b
-      b-UC⊆b {x} lt = ?
+      a-UC⊆a : * (& a-UC) ⊆ * a
+      a-UC⊆a {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
 
       open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
@@ -177,45 +178,31 @@
       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 ))  
 
-      be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
-      be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where
-          be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
-          be12 x lt = i→ g x ? where
-                be02 : odef (* b) x → ( ¬ CN x )
+      be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )
+      be10 = record { i→ = be12 ; iB = ? ; inject = be14 } where
+          be12 : (x : Ordinal) → odef (* (& a-UC)) x → Ordinal
+          be12 x lt = i→ g x (proj1 ? ) where
+                be02 : odef (* b) x ∧ ( ¬ CN ? )
                 be02 = ?
-          be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt)
-          be13 x lt = subst (λ k → odef k ?) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) ? ; x=fy = fba-eq refl } where
-                be02 : odef (* b) x →  ( ¬ CN x )
+          be13 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (& (Image (& a-UC) (Injection-⊆ a-UC⊆a ?)))) (be12 x lt)
+          be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) ? ; x=fy = fba-eq refl } where
+                be02 : odef (* b) x ∧ ( ¬ CN x )
                 be02 = ?
-          be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y
+          be14 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y
           be14 x y ltx lty eq = ? -- inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq
 
-      be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
-      be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where
-          be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal
-          be13 x lt with subst (λ k → odef k x) *iso lt 
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay))
-          be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt)
-          be14 x lt with subst (λ k → odef k x) *iso lt 
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
-          be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x)
-                (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) →
-                be13 x ltx ≡ be13 y lty → x ≡ y
-          be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty 
-          ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } 
-               =  trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) 
+      be11 : Injection  (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC)
+      be11 = record { i→ = ? ; iB = ? ; inject = ? } where
+          be13 : (x : Ordinal) → odef (* (& (Image (& a-UC) (Injection-⊆ a-UC⊆a ?)))) x → Ordinal
+          be13 x lt = ?
+          be14 : (x : Ordinal) (lt : odef (* (& (Image (& a-UC) ?))) x) → odef (* (& a-UC)) (be13 x lt)
+          be14 x lt = ?
      
-      b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx)  ≡ x
-      b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx)
-      ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ ? ? (sym x=fy) where
-                be02 : odef (* b) x ∧ ( ¬ CN x )
-                be02 = ?
-                be03 : odef (* b) y ∧ ( ¬ CN y )
-                be03 = ?
+      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 = ?
 
-      b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
-      b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx
-      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
+      a-UC-iso1 : (x : Ordinal ) → (cx : odef ? x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
+      a-UC-iso1 x cx = ?
 
       --   C n → f (C n) 
       fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
@@ -285,9 +272,9 @@
       ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
 
       Img∨ : (x : Ordinal) → (bx : odef (* b) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x 
-          ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (fba x bx) 
+          ∨ odef (* (& (Image (& a-UC) ?))) (fba x bx) 
       Img∨ x bx = be20 where
-             be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (fba x bx) 
+             be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& a-UC) ?))) (fba x bx) 
              be20 with ∨L＼X {* a} {UC} (a∋fba x bx)
              ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where
                  be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x
@@ -302,7 +289,7 @@
              be20 | case2 ⟪ agx , ncn ⟫ = be21 where
                  be22 :  ¬ odef (C 0) (fba x bx)  -- condition for g⁻¹
                  be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 }
-                 be21 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (fba x bx) 
+                 be21 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef ? (fba x bx) 
                  be21 with ODC.p∨¬p O (IsImage (& UC) _ (Injection-⊆ UC⊆a f) x) -- p∨¬p (CN (g⁻¹ agx be22) ) causes recursive record
                  ... | case1 cn  = case1 (subst (λ k → odef k x) (sym *iso)  cn )
                  ... | case2 ¬cn = case2 (subst (λ k → odef k (fba x bx)) (sym *iso) be32 ) where
@@ -316,19 +303,18 @@
                           be25 cn with CN.i cn | CN.gfix cn
                           ... | 0 | a-g ax ¬ib = ?
                           ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ?
-                          be32 : IsImage (& b-UC) _ (Injection-⊆ b-UC⊆b g) (fba x bx)
-                          be32 = record { y = x ; ay = ? ; x=fy = fba-eq refl }
+                          be32 : ?
+                          be32 = ?
 
       h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal
       h {x} ax with ODC.p∨¬p O ( CN x )
       ... | case1 cn  = fU x (subst (λ k → odef k x ) (sym *iso) cn)
-      ... | case2 ncn = i→ be10 (g⁻¹ ax ?) (subst (λ k → odef k (g⁻¹ ax ?) ) (sym *iso) (λ bx cngx → ? ) )
+      ... | case2 ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ )
 
       h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal
-      h⁻¹ {x} bx with ODC.p∨¬p O ( CN (fba x bx) )
-      ... | case1 cn  = fU (fba x bx) (subst (λ k → odef k (fba x bx) ) (sym *iso) cn )
-      ... | case2 ncn = i→ be11 (g⁻¹ (a∋fba x bx) ?) (subst (λ k → odef k (g⁻¹ (a∋fba x bx) ?)) (sym *iso) 
-          record { y = x ; ay = subst (λ k → odef k x) (sym *iso) (λ bx cngx → ?) ; x=fy = ? } )
+      h⁻¹ {x} bx with ODC.p∨¬p O ( CN x )
+      ... | case1 cn  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
+      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) ? )
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )