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

changeset 116:47541e86c6ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
axiom of selection
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jun 2019 08:05:58 +0900
parents 277c2f3b8acb
children a4c97390d312
files HOD.agda ordinal-definable.agda zf.agda
diffstat 3 files changed, 20 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Tue Jun 25 22:47:17 2019 +0900
+++ b/HOD.agda	Wed Jun 26 08:05:58 2019 +0900
@@ -48,8 +48,6 @@
    lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
    lemma {x}  x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
 
--- od∅ : {n : Level} → HOD {n} 
--- od∅ {n} = record { def = λ _ → Lift n ⊥ }
 od∅ : {n : Level} → HOD {n} 
 od∅ {n} = Ord o∅ 
 
@@ -60,7 +58,7 @@
   oiso   : {n : Level} {x : HOD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
-  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   -- necessary?
+  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
   -- supermum as Replacement Axiom
@@ -246,9 +244,9 @@
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = sup-od ψ
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → y o< od→ord X  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
-       lemma :  {x : Ordinal} → ((y : Ordinal) → y o< od→ord X → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
-            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → y₁ o< od→ord X → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
+    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
+       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
+            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
        lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
            y<X : X ∋ ord→od y
            y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
@@ -289,7 +287,7 @@
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
-       ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
+       ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement = replacement
      } where
          open _∧_ 
@@ -349,10 +347,11 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (( X ∋ y ) ∧ ψ y ) ⇔ (Select X ψ ∋ y)
+         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
          selection {X} {ψ} {y} =  record { proj1 = λ s → record {
-            proj1 = λ y → {!!}  ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord (ord→od (od→ord y))} (proj1 s) refl (sym diso) } ;
-            proj2 = {!!} }
+             proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
+           ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
+                                  ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
          replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
--- a/ordinal-definable.agda	Tue Jun 25 22:47:17 2019 +0900
+++ b/ordinal-definable.agda	Wed Jun 26 08:05:58 2019 +0900
@@ -315,7 +315,7 @@
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
     Replace X ψ = sup-od ψ
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
-    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) } 
+    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}
     x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
     Union : OD {suc n} → OD {suc n}
@@ -411,11 +411,13 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection : {ψ : OD → Set (suc n)} {X y : OD} →  (((y : OD) → X ∋ y → ψ y) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
          selection {ψ} {X} {y} = record {
-              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
-            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-           }
+              proj1 = λ cond → record { proj1 = λ y X>y → proj1 cond (ord→od y) (subst (λ k → def X k ) (sym diso) X>y) ; proj2 = proj2 cond }
+            ; proj2 = λ select → record { proj1 = λ y X>y → subst (λ k → ψ k ) oiso (proj1 select (od→ord y) X>y )  ; proj2 =  proj2 select } 
+           } where
+               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}
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
@@ -430,8 +432,8 @@
             lemma (case1 ())
             lemma (case2 ())
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
-            reg {y} t with proj1 t
-            ... | x∈∅ = x∈∅
+            reg {y} t with proj1 t y (proj2 t)
+            ... | x∈∅ = o<-subst (proj1 x∈∅) diso refl
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
--- a/zf.agda	Tue Jun 25 22:47:17 2019 +0900
+++ b/zf.agda	Wed Jun 26 08:05:58 2019 +0900
@@ -15,7 +15,7 @@
    case1 : A → A ∨ B
    case2 : B → A ∨ B
 
-_⇔_ : {n : Level } → ( A B : Set n )  → Set  n
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
 open import Relation.Nullary
@@ -74,7 +74,7 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
+     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 ψ )  
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]