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

changeset 1407:523bd51605cb

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 Thu, 29 Jun 2023 18:56:57 +0900
parents ba377f7d0c40
children 2fe6908fb48e
files src/cardinal.agda
diffstat 1 files changed, 8 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Thu Jun 29 16:58:43 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 18:56:57 2023 +0900
@@ -196,9 +196,11 @@
       be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )
       be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = ? } where
           be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
-          be15 = ?
+          be15 {x} lt with subst (λ k → odef k x) *iso lt
+          ... | ⟪ ax , ncn ⟫ = ax
           be16 : {x : Ordinal } → odef (* (& a-UC)) x → ¬ odef (C 0) x
-          be16 = ? 
+          be16 {x} lt nc0 with subst (λ k → odef k x) *iso lt
+          ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn record { i = 0 ; gfix = nc0 } )
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
           be17 = ?
 
@@ -277,24 +279,11 @@
       ... | case2 ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ )
 
       h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal
-      h⁻¹ {x} bx with ODC.p∨¬p O ( CN (fba x bx ))
-      ... | case1 cn  = be63 where -- Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } )
-           be63 : Ordinal
-           be63 with CN.i cn | CN.gfix cn
-           ... | 0 | a-g ax ¬ib = Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } )
-           ... | suc i | next-gf {px} ix t = Uf (fab px ?) (subst (λ k → odef k (fab px ?) ) (sym *iso) 
-               record { y = _ ; ay = subst (λ k → odef k (fab px ?)) (sym *iso) record { i = ? ; gfix = ? } ; x=fy = ? } )
-      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where
-           be61 : ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x
-           be61 record { y = y ; ay = ay ; x=fy = x=fy } = be62 where
-               cny : CN y
-               cny = subst (λ k → odef k y ) *iso ay 
-               be62 : ⊥
-               be62 with CN.i cny | CN.gfix cny
-               ... | 0 | a-g ax ¬ib = ncn record { i = 1 ; gfix = next-gf  record { y = _ ; ay = ax ; x=fy = fba-eq x=fy } (a-g ax ¬ib) }
-               ... | suc i | t = ncn record { i = suc (suc i) ; gfix = next-gf  record { y = _ ; ay = ? ; x=fy = fba-eq x=fy } t }
+      h⁻¹ {x} bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
+      ... | case1 cn  = Uf x (subst (λ k → odef k x) (sym *iso) cn)                    --   x ≡ f y
+      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where     -- ¬ x ≡ f y
            be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-           be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) be61 ⟫
+           be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
 
 
 _c<_ : ( A B : HOD ) → Set n