# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688189180 -32400
# Node ID 77a3de21ee50e7deeb186008b0a5e48a53a5cfdd
# Parent  ee40c5b5cefed55c017b9c4c0e09352501a6b17a
...

diff -r ee40c5b5cefe -r 77a3de21ee50 src/cardinal.agda
--- a/src/cardinal.agda	Sat Jul 01 10:19:03 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 14:26:20 2023 +0900
@@ -247,6 +247,11 @@
       ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy )
       ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl })
 
+      a-UC-iso11 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) 
+           → (ib : odef (* (& a-UC)) (fba x ( proj1 ( subst (λ k → odef k x) (*iso) cx )) ))
+           → i→ be10 ( i→ be11 x cx ) ib  ≡ x
+      a-UC-iso11 x cx ib = trans ? (a-UC-iso1 x cx)
+
       --   C n → f (C n) 
       fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
       fU x lt = be03 where
@@ -411,31 +416,24 @@
       ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) 
          = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 
              ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) })
-      ... | case2 c2  = be80 where
+      ... | case2 c2  = ? where -- a-UC-iso11 x be79 (subst (λ k → odef k (fba x (proj1 (subst (λ k₁ → odef k₁ x) *iso be79 )  ))) (sym *iso) be77 ) where
            be79 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )) x
-           be79 = subst (λ k → odef k x) (sym *iso) ⟪ bx , subst (λ k → odef k x → ⊥) (sym *iso) x₁ ⟫
+           be79 = proj1 (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) ⟪ bx , subst (λ k → odef k x → ⊥) (sym *iso) x₁ ⟫))
            bx1 : odef (* b) x
            bx1 = proj1 (subst (λ k → odef k x) *iso be79)
-           be77 : odef (Image b g) (fba x (proj1 (subst (λ k → odef k x) *iso be79)) )
-           be77 = nimg (a∋fba x (proj1 (subst (λ k → odef k x) *iso be79))) c2
-           be80 : g⁻¹ ? ? ≡ x
-           be80 = ?
-
-      -- with ODC.p∨¬p O ( IsImage b a g (fba x bx ))
-      -- ... | case1 (img @ record { y = y ; ay = ay ; x=fy = x=fy }) = trans (ImageUnique ? ? ) (sym ( inject g _ _ bx ay x=fy )) where
-      --      be79 : odef (* b) x
-      --      be79 = proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) 
-      --             ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))
-      --      be78 : odef (Image b g) ?
-      --      be78 = nimg (a∋fba ? ?) c2
-      --      be77 : odef (Image b g) (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) 
-      --             ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫)))) 
-      --      be77 = nimg (a∋fba ? ?) c2
-      -- ... | case2 ¬img = ?
-
+           be77 : odef a-UC (fba x bx1 )
+           be77 = subst (λ k → odef k (fba x bx)) *iso (subst (λ k → odef k (fba x bx)) (sym *iso) ⟪ bx , subst (λ k → odef k (fba x bx) → ⊥) (sym *iso) x₁ ⟫)
+           be80 : odef (* (& a-UC)) (fba x bx1 )
+           be80 = 
+                  (subst (λ k → odef k (fba x (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso)
+                     ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫)))))
+              (sym *iso)
+              ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x (proj1
+                     (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso)
+                       ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso) ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , ? ⟫)) , c2 ⟫)
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x
       be73 x ax (case1 x₁) with cc11 ax (case1 x₁)
-      ... | case1 c1 = ? where
+      ... | case1 c1 = trans ? be76 where
             be76 : IsImage.y (subst (λ k → odef k (fU x (subst (λ k₁ → odef k₁ x) (sym *iso) x₁))) *iso (be04 (subst (λ k → odef k x) (sym *iso) x₁))) ≡ x
             be76 = UC-iso0 x (subst (λ k → odef k x) (sym *iso) x₁ )
       ... | case2 c2 = ?