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

comparison zf.agda @ 29:fce60b99dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
posturate OD is isomorphic to Ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 May 2019 18:18:43 +0900
parents 7293a151d949
children 3b0fdb95618e
comparison
equal deleted inserted replaced
28:f36e40d5d2c3 29:fce60b99dc55
53 (Select : ZFSet → ( ZFSet → Set m ) → ZFSet ) 53 (Select : ZFSet → ( ZFSet → Set m ) → ZFSet )
54 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet ) 54 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
55 (infinite : ZFSet) 55 (infinite : ZFSet)
56 : Set (suc (n ⊔ m)) where 56 : Set (suc (n ⊔ m)) where
57 field 57 field
58 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ 58 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
59 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) 59 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
60 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) 60 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B )
61 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x)) 61 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x))
62 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y 62 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y
63 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y 63 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y