Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 )))