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

changeset 1415:85842347e270

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
work around on strict positive on gfImage
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Jun 2023 19:03:50 +0900
parents 180caeb6927b
children 4d9b60eed372
files src/cardinal.agda
diffstat 1 files changed, 27 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Fri Jun 30 18:10:40 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 19:03:50 2023 +0900
@@ -124,12 +124,13 @@
 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←  = λ x lt → ?
-       ; fun→  = λ x lt → ?
+         fun←  = λ x lt → h lt (cc0 x)
+       ; fun→  = λ x lt → h⁻¹ lt (cc1 x)
        ; funB  = ?
        ; funA  = ?
-       ; fiso← = ?
-       ; fiso→ = ? }
+       ; fiso← = λ x lt → be72 x lt (cc1 x) 
+       ; fiso→ = λ x lt → be73 x lt (cc0 x)   
+       }
  where
       gf : Injection a a
       gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
@@ -296,6 +297,18 @@
             ... | a-g ax ¬ib = sym x=fy
             ... | next-gf t ix = sym x=fy
 
+      CC0 : (x : Ordinal) → Set n
+      CC0 x =  gfImage x ∨ (¬ gfImage x) 
+
+      CC1 : (x : Ordinal) → Set n
+      CC1 x =  odef (Image (& UC) (Injection-⊆ UC⊆a f)) x ∨ (¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) 
+
+      cc0 : (x : Ordinal) → CC0 x
+      cc0 x = ODC.p∨¬p O (gfImage x) 
+
+      cc1 : (x : Ordinal) → CC1 x
+      cc1 x = ODC.p∨¬p O (odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) 
+
       h : {x : Ordinal } → (ax : odef (* a) x) → gfImage x ∨ (¬ gfImage x) → Ordinal
       h {x} ax (case1 cn)  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
       h {x} ax (case2 ncn) = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) 
@@ -335,10 +348,16 @@
       be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) 
       be70-1 = ?
 
-      be72 :  (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx ?) ? ≡ x
-      be72 x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) 
-      be72 x bx | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ?
-      be72 x bx | case2 nimg = ?
+      cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → CC0 (h⁻¹ bx cc1 ) 
+      cc10 = ?
+
+      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
+      be72 x bx (case1 x₁)  = trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
+      be72 x bx (case2 x₁)  = trans ? (a-UC-iso1 x ? )
+
+      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ ? ? ≡ x
+      be73 x bx (case1 x₁)  = trans ? (UC-iso0 x (subst (λ k → odef k x) (sym *iso) ? ))
+      be73 x bx (case2 x₁)  = trans ? (a-UC-iso0 x ? )
 
 
 _c<_ : ( A B : HOD ) → Set n