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

changeset 130:3849614bef18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new replacement axiom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 02 Jul 2019 15:59:07 +0900
parents 2a5519dcc167
children 5dcd5a3583a0
files HOD.agda ordinal-definable.agda zf.agda
diffstat 3 files changed, 24 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Tue Jul 02 09:28:26 2019 +0900
+++ b/HOD.agda	Tue Jul 02 15:59:07 2019 +0900
@@ -342,7 +342,10 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-       ;   replacement = replacement
+       ;   reverse = ?
+       ;   reverse-∈ = ?
+       ;   replacement← = ?
+       ;   replacement→ = ?
      } where
 
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
@@ -375,6 +378,7 @@
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
+              -- lemma1 hold because minsup is Ord (minα a sp) 
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
               lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
               ... | eq with subst ( λ k →  ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq
@@ -391,7 +395,6 @@
                     ≡⟨ sym eq1 ⟩
                       minsup
                     ∎
-
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
@@ -410,10 +413,18 @@
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
+         -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
          power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
          power→ = {!!}
          power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← = {!!}
+         power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} (sup-c< ψ {t}) lemma2 lemma1 where
+              a = od→ord A
+              ψ : HOD → HOD
+              ψ y = Def (Ord a) ∩ y
+              lemma1 : od→ord (Def (Ord a) ∩ t) ≡ od→ord t
+              lemma1 = {!!} 
+              lemma2 : Ord ( sup-o ( λ x → od→ord (ψ (ord→od x )))) ≡ Power A
+              lemma2 = {!!}
 
          union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
--- a/ordinal-definable.agda	Tue Jul 02 09:28:26 2019 +0900
+++ b/ordinal-definable.agda	Tue Jul 02 15:59:07 2019 +0900
@@ -308,7 +308,7 @@
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
-    Replace X ψ = sup-od ψ
+    Replace X ψ = record { def = λ x → ( X ∋ ord→od x ) ∧ (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) }
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
     Select X ψ = record { def = λ x →  ((y : Ordinal {suc n}) → def X y → ψ ( ord→od y )) ∧ def X x  } 
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
@@ -346,7 +346,10 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} 
-       ;   replacement = replacement
+       ;   repl-x = λ {ψ} {X} {x} lt → Ord (sup-x (λ x → od→ord (ψ (ord→od x))))
+       ;   repl-x-∈ = λ {ψ} {X} {x} lt  → {!!}
+       ;   replacement← = {!!}
+       ;   replacement→ = {!!}
      } where
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
@@ -412,7 +415,7 @@
                lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y
                lemma cond = (proj1 cond) y (proj2 cond)
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
-         replacement {ψ} X x = sup-c< ψ {x}
+         replacement {ψ} X x = {!!} -- sup-c< ψ {x}
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
--- a/zf.agda	Tue Jul 02 09:28:26 2019 +0900
+++ b/zf.agda	Tue Jul 02 15:59:07 2019 +0900
@@ -77,7 +77,10 @@
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
      selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
-     replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )  
+     repl-x : {ψ : ZFSet → ZFSet} → { X x : ZFSet  }  ( lt : x ∈  Replace X ψ ) →  ZFSet
+     repl-x-∈ : {ψ : ZFSet → ZFSet} → { X x : ZFSet  } →  (lt : x ∈  Replace X ψ ) →  repl-x lt ∈ X
+     replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ 
+     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → x ≈ ψ ( repl-x lt )  
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
    -- axiom-of-choice : Set (suc n) 
    -- axiom-of-choice = ?