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

changeset 186:914cc522c53a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix extensionality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2019 18:49:38 +0900
parents a002ce0346dd
children ac872f6b8692
files OD.agda zf.agda
diffstat 2 files changed, 9 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 22 18:36:45 2019 +0900
+++ b/OD.agda	Mon Jul 22 18:49:38 2019 +0900
@@ -292,7 +292,7 @@
        ;   empty = empty
        ;   power→ = power→  
        ;   power← = power← 
-       ;   extensionality = extensionality
+       ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
        ;   ε-induction = ε-induction
        ;   infinity∅ = infinity∅
        ;   infinity = infinity
@@ -441,9 +441,13 @@
              lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
              lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
 
-         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  
+         extensionality0 : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+         eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
+         eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+
+         extensionality : {A B w : OD {suc n} } → ((z : OD {suc n}) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
+         proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
+         proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
          infinity∅ : infinite  ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where
--- a/zf.agda	Mon Jul 22 18:36:45 2019 +0900
+++ b/zf.agda	Mon Jul 22 18:49:38 2019 +0900
@@ -70,7 +70,7 @@
      power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} 
      power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
-     extensionality :  { A B : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → A ≈ B
+     extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
      -- This form of regurality forces choice function
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
      -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet