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

changeset 1413:c66ee9d43c05

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 Fri, 30 Jun 2023 16:37:32 +0900
parents 4b72bc3e2fab
children 180caeb6927b
files src/cardinal.agda
diffstat 1 files changed, 10 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Fri Jun 30 15:08:29 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 16:37:32 2023 +0900
@@ -297,9 +297,9 @@
             ... | next-gf t ix = sym x=fy
 
       h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal
-      h {x} ax with ODC.∋-p O UC (* x)
-      ... | yes cn  = fU x (subst (λ k → odef k x ) (sym *iso) (subst (λ k → gfImage k) &iso cn) )
-      ... | no ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , subst (λ k → ¬ (gfImage k)) &iso ncn ⟫ )
+      h {x} ax with ODC.p∨¬p O (gfImage x)
+      ... | case1 cn  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
+      ... | 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 (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
@@ -330,38 +330,13 @@
            be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx) ≡ x
-      be72 x bx = ? where
-
-           be76 : (cn : odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) → h⁻¹ bx ≡ Uf x (subst (λ k → odef k x) (sym *iso) cn)
-           be76 cn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
-           ... | case1 img = cong (λ k →  Uf x k ) ( HE.≅-to-≡ ( ∋-irr {(* (& (Image (& UC) (Injection-⊆ UC⊆a f))))} b04 b05 )) where
-               b04 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-               b04 = subst (λ k → odef k x) (sym *iso) img
-               b05 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-               b05 = subst (λ k → odef k x) (sym *iso) cn
-           ... | case2 nimg = ⊥-elim ( nimg cn)
-
-           be73 : (cn : odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) → odef (* a) (Uf x (subst (λ k → odef k x) (sym *iso) cn))
-           be73 cn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
-           ... | case1 img = be03 (subst (λ k → odef k x) (sym *iso) cn) where
-               be03 : (cn : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* a) (Uf x cn )
-               be03 cn with subst (λ k → odef k x ) *iso cn
-               ... | record { y = y ; ay = ay ; x=fy = x=fy } = UC⊆a ay
-           ... | case2 nimg = ⊥-elim ( nimg cn)
-
-           be60 : (ncn : ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) → odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-           be60 ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
-           be74 : (ncn : ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) → odef (* a) (i→ be11 x (subst (λ k → odef k x ) (sym *iso) (be60 ncn) )) 
-           be74 ncn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
-           ... | case1 img = ⊥-elim ( ncn img )
-           ... | case2 nimg = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) (be60 ncn)) ))   
-
-           be75 : h (be71 x bx) ≡ x
-           be75 with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)
-           ... | case1 cn  = ? where --  trans ? (be78 (be73 cn)) where
-                be78 : (auf : odef (* a) (Uf x (subst (λ k → odef k x) (sym *iso) cn))) → h auf ≡ x
-                be78 = ?
-           ... | case2 ncn = ?
+      be72 x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) 
+      be72 x bx | case1 img = ? where
+           be73 : gfImage (Uf x (subst (λ k → odef k x) (sym *iso) img ))
+           be73 = ?
+           be74 : Uf x (subst (λ k → odef k x) (sym *iso) img ) ≡ IsImage.y (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) img))
+           be74 = refl
+      be72 x bx | case2 nimg = ?
 
 
 _c<_ : ( A B : HOD ) → Set n