# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688229123 -32400
# Node ID 8da1d318033b3df073f03f9b9cfbaa237858c22b
# Parent  052f0fca77994d2b94dd0e7f404dcaa3084e0eb1
...

diff -r 052f0fca7799 -r 8da1d318033b src/cardinal.agda
--- a/src/cardinal.agda	Sun Jul 02 00:59:14 2023 +0900
+++ b/src/cardinal.agda	Sun Jul 02 01:32:03 2023 +0900
@@ -134,8 +134,8 @@
        ; fun→  = λ x lt → h⁻¹ lt (cc1 x)
        ; funB  = λ x lt → be74 x lt (cc0 x)
        ; funA  = λ x lt → be75 x lt (cc1 x)
-       ; fiso← = λ x lt → be72 x lt (cc1 x)
-       ; fiso→ = λ x lt → be73 x lt (cc0 x)
+       ; fiso← = λ x bx → be72 x bx (cc1 x) (cc0 (h⁻¹ bx (cc1 x)))
+       ; fiso→ = λ x ax → be73 x ax (cc0 x) (cc1 (h ax (cc0 x)))
        }
  where
       gf : Injection a a
@@ -434,15 +434,14 @@
       ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
       ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))
 
-      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x ) →  h (be75 x bx cc1) (cc0 (h⁻¹ bx cc1)) ≡ x
-      be72 x bx (case1 x₁) with cc0 (Uf1 x x₁)
-      ... | t = ?
-      be72 x bx (case2 x₁) = ?
+      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x ) (cc0 : CC0 (h⁻¹ bx cc1)) →  h (be75 x bx cc1) cc0 ≡ x
+      be72 x bx (case1 x₁) t = ?
+      be72 x bx (case2 x₁) t = ?
 
 
-      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be74 x ax cc0) (cc1 (h ax cc0)) ≡ x
-      be73 x ax (case1 x₁) = ?
-      be73 x ax (case2 x₁) = ?
+      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) (cc1 : CC1 (h ax cc0)) →  h⁻¹ (be74 x ax cc0) cc1  ≡ x
+      be73 x ax (case1 x₁) t = ?
+      be73 x ax (case2 x₁) t = ?
 
 
 _c<_ : ( A B : HOD ) → Set n