Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1432:8da1d318033b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jul 2023 01:32:03 +0900
parents 052f0fca7799
children ea470857db44
files src/cardinal.agda
diffstat 1 files changed, 8 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- 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