diff zf.agda @ 186:914cc522c53a

fix extensionality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2019 18:49:38 +0900
parents de3d87b7494f
children 1f2c8b094908
line wrap: on
line diff
--- 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