# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688267334 -32400
# Node ID 2d7341d4a90aa6c9a33361192c7b2de056891b23
# Parent  52853b81df80555045dfdcb84df588f1235d9be0
...

diff -r 52853b81df80 -r 2d7341d4a90a src/cardinal.agda
--- a/src/cardinal.agda	Sun Jul 02 10:35:37 2023 +0900
+++ b/src/cardinal.agda	Sun Jul 02 12:08:54 2023 +0900
@@ -366,7 +366,7 @@
       b∋Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋fab y (a∋gfImage ay))
 
       Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
-      Uf1 x lt = fba x (b∋Uf1 x lt) 
+      Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = y
 
       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
@@ -426,22 +426,39 @@
       cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) 
       cc21 {x} lt = cc1 (fab x lt)
 
+      UC∋Uf1 : {x : Ordinal } → (lt : odef fUC x) → odef UC (Uf1 x lt )
+      UC∋Uf1 {x} record { y = y ; ay = ay ; x=fy = x=fy } = ay
+
+      fU-iso1 : {x : Ordinal } → (lt : odef fUC x) → fU1 (Uf1 x lt) (UC∋Uf1 lt) ≡ x
+      fU-iso1 {x} record { y = y ; ay = (a-g ax ¬ib) ; x=fy = x=fy } = trans (fab-eq refl) (sym x=fy) 
+      fU-iso1 {x} record { y = y ; ay = (next-gf record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ } ay) ; x=fy = x=fy } = trans (fab-eq refl) (sym x=fy) 
+
+      fU-iso0 : {x : Ordinal } → (lt : odef UC x) → Uf1 (fU1 x lt) record { y = _ ; ay = lt ; x=fy = refl } ≡ x
+      fU-iso0 {x} (a-g ax ¬ib) = ?
+      fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = ?
+
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
          fun←  = λ x lt → fU1 x lt
        ; fun→  = λ x lt → Uf1 x lt
-       ; funB  = λ x lt → ?
-       ; funA  = λ x lt → ?
-       ; fiso← = λ x lt → ?
-       ; fiso→ = λ x lt → ?
+       ; funB  = λ x lt → record { y = _ ; ay = lt  ; x=fy = refl }
+       ; funA  = λ x lt → UC∋Uf1 lt
+       ; fiso← = λ x lt → fU-iso1 lt
+       ; fiso→ = λ x lt → fU-iso0 lt
        }
 
+      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 (fba x (proj1 lt ))
+      a-UC∋g {x} ⟪ bx , ¬img ⟫ = ⟪ a∋fba x bx , cc10-case2 bx ¬img ⟫
+
       bi-fUC : HODBijection a-UC b-fUC
       bi-fUC = record { 
          fun←  = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))
        ; fun→  = λ x lt → fba x (proj1 lt)
-       ; funB  = λ x lt → ?
-       ; funA  = λ x lt → ?
+       ; funB  = λ x lt → b-FUC∋g⁻¹  lt
+       ; funA  = λ x lt → a-UC∋g lt
        ; fiso← = λ x lt → ?
        ; fiso→ = λ x lt → ?
        }
@@ -468,7 +485,7 @@
 
       cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x ) → CC0 (h⁻¹ bx cc1 ) 
       cc10 {x} bx (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = 
-          case1 (next-gf record { y = _ ; ay = a∋gfImage ay ; x=fy = fba-eq x=fy } ay )
+          case1 (next-gf record { y = _ ; ay = a∋gfImage ay ; x=fy = ? } ay )
       cc10 {x} bx (case2 x₁) = case2 (cc10-case2 bx x₁ ) 
 
       cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ) → CC1 (h ax cc0 ) 
@@ -480,7 +497,7 @@
       be70 x ax ( case2 ncn ) = b∋g⁻¹ ax (nimg ax ncn)
 
       be71 :  (x : Ordinal) (bx : odef (* b) x) → (or : CC1 x) → odef (* a) (h⁻¹ bx or )
-      be71  x bx ( case1 cn ) = subst (λ k → odef (* a) k) (fba-eq refl) (a∋fba x bx  )
+      be71  x bx ( case1 cn ) = ?
       be71 x bx ( case2 ncn ) = a∋fba x bx 
 
       be71-1 :  (x : Ordinal) (bx : odef (* b) x)