# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688000489 -32400
# Node ID 5476e93726e308cc2e70f6fb94254cfa35ef2e3e
# Parent  d9eb3ae5fbad91fbc6a2b03da530a7c95a3856d1
...

diff -r d9eb3ae5fbad -r 5476e93726e3 src/cardinal.agda
--- a/src/cardinal.agda	Thu Jun 29 07:08:32 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 10:01:29 2023 +0900
@@ -155,7 +155,7 @@
       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 → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt)  }
+      b-UC = record { od = record { def = λ x → (bx : odef (* b) x) →  ¬ CN (fba x bx) } ; odmax = & (* b) ; <odmax = λ lt → ? } -- odef< (proj1 lt)  }
       
       --  UC ⊆ * a
       --     f : UC → Image f UC    is injection
@@ -167,7 +167,7 @@
             be02 = subst (λ k → odef k x) *iso lt
 
       b-UC⊆b : * (& b-UC) ⊆ * b
-      b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
+      b-UC⊆b {x} lt = ?
 
       open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
@@ -180,15 +180,15 @@
       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 (proj1 be02) where
-                be02 : odef (* b) x ∧ ( ¬ CN x )
-                be02 = subst (λ k → odef k x) *iso lt
+          be12 x lt = i→ g x ? where
+                be02 : odef (* b) x → ( ¬ CN x )
+                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 (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-eq refl } where
-                be02 : odef (* b) x ∧ ( ¬ CN x )
-                be02 = subst (λ k → odef k x) *iso 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 )
+                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 ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq
+          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
@@ -207,11 +207,11 @@
      
       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 _ _ (proj1 be03) (proj1 be02) (sym x=fy) where
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ ? ? (sym x=fy) where
                 be02 : odef (* b) x ∧ ( ¬ CN x )
-                be02 = subst (λ k → odef k x) *iso cx
+                be02 = ?
                 be03 : odef (* b) y ∧ ( ¬ CN y )
-                be03 = subst (λ k → odef k y) *iso ay
+                be03 = ?
 
       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
@@ -299,33 +299,36 @@
                      be24 = inject g _ _ bx (b∋fab y ay) x=fy
                      be25 : odef UC y
                      be25 = record { i = i ; gfix = t }
-             be20 | case2 ⟪ agx , ncn ⟫ = case2 (subst (λ k → odef k (fba x bx) ) (sym *iso) be21 ) where
-                 be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) (fba x bx) 
-                 be21 = record { y = g⁻¹ agx  be22
-                      ; ay = subst (λ k → odef k (g⁻¹ agx  be22)) (sym *iso) ⟪ b∋g⁻¹ agx be22 , be23 ⟫  ; x=fy = ? } where
-                          be22 :  ¬ odef (C 0) (fba x bx) 
-                          be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 }
+             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 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
+                          be23 : x ≡ g⁻¹ agx be22
+                          be23 = inject g _ _ bx (b∋g⁻¹ agx be22) (sym (g⁻¹-iso agx be22 ))
                           be30 : CN (fba x bx) → ⊥ 
                           be30 = ncn
-                          be25 : ¬ CN (g⁻¹ agx be22)  
-                          be25 cn = be26 (CN.i cn) _ ? (CN.gfix cn) ?  where
-                             be26 : (i : ℕ) (y : Ordinal) (ay : odef (* a) y)  ( gfi : gfImage i  y ) → ¬ CN y  → ⊥
-                             be26 0 y ay (a-g ax ¬ib) ncy = ⊥-elim ( ncy record { i = 0 ; gfix = a-g ax ¬ib } )
-                             be26 (suc i) y ay (next-gf record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } gfi) ncy = be26 i y1 ay1 gfi be27 where
-                                 be27 : ¬ (CN y1)
-                                 be27 cn with CN.i cn | CN.gfix cn
-                                 ... | 0 | t @ (a-g ax ¬ib) = ncy record { i = suc 0 
-                                    ; gfix = next-gf record { y = y1 ; ay = ax ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) }  t }
-                                 ... | suc i | t @ (next-gf ix t1) = ncy record { i = suc (suc i) 
-                                    ; gfix = next-gf record { y = y1 ; ay = a∋gfImage _ t ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) } t }
-                          be23 : ¬ CN (g⁻¹ agx be22)  -- g⁻¹ (g x ) -- ¬ CN x
-                          be23 cng with CN.i cng | CN.gfix cng
-                          ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = ? ; ay = ? ; x=fy = ? } )
-                          ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? })
-                          be24 : ¬ CN x  
-                          be24 cng with CN.i cng | CN.gfix cng
-                          ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = g⁻¹ agx be22 ; ay = ? ; x=fy = ? } )
-                          ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? })
+                          be31 : ¬ IsImage (& UC) _ (Injection-⊆ UC⊆a f) x
+                          be31 = ¬cn
+                          be25 : ¬ CN x  
+                          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 }
+
+      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 → ? ) )
+
+      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 = ? } )
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )