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

changeset 1436:d6a0ecafff80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Bernstein done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jul 2023 14:39:47 +0900
parents 2d7341d4a90a
children 6cac0f746c83
files src/cardinal.agda
diffstat 1 files changed, 12 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sun Jul 02 12:08:54 2023 +0900
+++ b/src/cardinal.agda	Sun Jul 02 14:39:47 2023 +0900
@@ -434,8 +434,8 @@
       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) = ?
+      fU-iso0 {x} (a-g ax ¬ib) = refl 
+      fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = refl
 
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
@@ -453,14 +453,22 @@
       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 ⟫
 
+      fUC-iso1 : {x : Ordinal } → (lt : odef b-fUC x ) → g⁻¹ (proj1 (a-UC∋g lt)) (nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))) ≡ x
+      fUC-iso1 {x} lt with nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 lt) ay x=fy )
+
+      fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) →  fba (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) (proj1 (b-FUC∋g⁻¹ lt)) ≡ x
+      fUC-iso0 {x} lt with nimg (proj1 lt) (proj2 lt)
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
+
       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 → b-FUC∋g⁻¹  lt
        ; funA  = λ x lt → a-UC∋g lt
-       ; fiso← = λ x lt → ?
-       ; fiso→ = λ x lt → ?
+       ; fiso← = λ x lt → fUC-iso1 lt
+       ; fiso→ = λ x lt → fUC-iso0 lt
        }
 
       --