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

changeset 1411:e5192c07777f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive record CN needs to be declared as either inductive or coinductive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Jun 2023 12:22:26 +0900
parents cc76e2b1f3b5
children 4b72bc3e2fab
files src/cardinal.agda
diffstat 1 files changed, 18 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Fri Jun 30 11:30:04 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 12:22:26 2023 +0900
@@ -339,6 +339,16 @@
 
       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
@@ -346,6 +356,7 @@
                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) )) 
@@ -353,6 +364,13 @@
            ... | 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  = 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 = ?
+
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )