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

changeset 1401:34f72406fcfd

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 02:36:06 +0900
parents 1c7b0a040d9c
children d9eb3ae5fbad
files src/ODC.agda src/cardinal.agda
diffstat 2 files changed, 46 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Wed Jun 28 14:02:57 2023 +0900
+++ b/src/ODC.agda	Thu Jun 29 02:36:06 2023 +0900
@@ -94,6 +94,11 @@
 or-exclude {A} {B} (case2 b) | case1 a = case1 a
 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
 
+or-exclude1 : {A B : Set n} →  (¬ A →  B ) → A ∨ B 
+or-exclude1 {A} {B} ab with p∨¬p A
+... | case1 a = case1 a
+... | case2 ¬a = case2 ( ab ¬a)
+
 -- record By-contradiction (A : Set n) (B : A → Set n)  : Set (suc n) where
 --  field
 --     a : A
--- a/src/cardinal.agda	Wed Jun 28 14:02:57 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 02:36:06 2023 +0900
@@ -123,7 +123,8 @@
 
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })
-     = record { fun←  = ?
+     = record { 
+         fun←  = ?
        ; fun→  = ?
        ; funB  = ?
        ; funA  = ?
@@ -268,9 +269,25 @@
              ... | 0 | a-g ax ¬ib = sym x=fy
              ... | (suc i) | next-gf t ix = sym x=fy
 
-      Img∨ : (x : Ordinal) → odef (* b) x → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x 
+      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → ¬ odef (C 0) x → Ordinal
+      g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
+      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = y
+      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+
+      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x) → odef (* b) (g⁻¹ ax nc0)
+      b∋g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
+      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ay
+      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+
+      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
+      g⁻¹-iso {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
+      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
+      ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
+
+      Img∨ : (x : Ordinal) → (bx : odef (* b) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x 
+          ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (fba x bx) 
       Img∨ x bx = be20 where
-             be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x 
+             be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (fba x bx) 
              be20 with ∨L＼X {* a} {UC} (a∋fba x bx)
              ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where
                  be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x
@@ -282,9 +299,27 @@
                      be24 = inject g _ _ bx (b∋fab y ay) x=fy
                      be25 : odef UC y
                      be25 = record { i = i ; gfix = t }
-             be20 | case2 ⟪ agx , ncn ⟫ = case2 (subst (λ k → odef k x) (sym *iso) be21 ) where
-                 be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) x
-                 be21 = record { y = ? ; ay = ? ; x=fy = ? }
+             be20 | case2 ⟪ agx , ncn ⟫ = case2 (subst (λ k → odef k (fba x bx) ) (sym *iso) be21 ) where
+                 be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) (fba x bx) 
+                 be21 = record { y = g⁻¹ agx  be22
+                      ; ay = subst (λ k → odef k (g⁻¹ agx  be22)) (sym *iso) ⟪ b∋g⁻¹ agx be22 , be23 ⟫  ; x=fy = ? } where
+                          be22 :  ¬ odef (C 0) (fba x bx) 
+                          be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 }
+                          be30 : CN (fba x bx) → ⊥ 
+                          be30 = ncn
+                          be25 : ¬ CN (g⁻¹ agx be22)  
+                          be25 = ? where
+                             be26 : (i : ℕ) (y : Ordinal) (ay : odef (* a) y)  ( gfi : gfImage i  y ) → ¬ CN (fab y ay )  → ⊥
+                             be26 0 y ay (a-g ax ¬ib) ncy = ?
+                             be26 (suc i) y ay (next-gf record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } gfi) ncy = be26 i y1 ay1 gfi ?
+                          be23 : ¬ CN (g⁻¹ agx be22)  -- g⁻¹ (g x ) -- ¬ CN x
+                          be23 cng with CN.i cng | CN.gfix cng
+                          ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = ? ; ay = ? ; x=fy = ? } )
+                          ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? })
+                          be24 : ¬ CN x  
+                          be24 cng with CN.i cng | CN.gfix cng
+                          ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = g⁻¹ agx be22 ; ay = ? ; x=fy = ? } )
+                          ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? })
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )