diff zf.agda @ 247:d09437fcfc7c

fix pair
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 12:27:20 +0900
parents 650bdad56729
children 63df67b6281c
line wrap: on
line diff
--- a/zf.agda	Mon Aug 26 02:50:16 2019 +0900
+++ b/zf.agda	Mon Aug 26 12:27:20 2019 +0900
@@ -22,8 +22,9 @@
        : Set (suc (n ⊔ m)) where
   field
      isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 
-     -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
-     pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
+     -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t  ≈ y)
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
      -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
      union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
      union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))