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

comparison zf.agda @ 115:277c2f3b8acb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Select declaration
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Jun 2019 22:47:17 +0900
parents 1daa1d24348c
children 47541e86c6ac
comparison
equal deleted inserted replaced
114:89204edb71fa 115:277c2f3b8acb
34 (_≈_ : Rel ZFSet m) 34 (_≈_ : Rel ZFSet m)
35 (∅ : ZFSet) 35 (∅ : ZFSet)
36 (_,_ : ( A B : ZFSet ) → ZFSet) 36 (_,_ : ( A B : ZFSet ) → ZFSet)
37 (Union : ( A : ZFSet ) → ZFSet) 37 (Union : ( A : ZFSet ) → ZFSet)
38 (Power : ( A : ZFSet ) → ZFSet) 38 (Power : ( A : ZFSet ) → ZFSet)
39 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → X ∋ x → Set m ) → ZFSet ) 39 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
40 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet ) 40 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
41 (infinite : ZFSet) 41 (infinite : ZFSet)
42 : Set (suc (n ⊔ m)) where 42 : Set (suc (n ⊔ m)) where
43 field 43 field
44 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 44 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
51 _∈_ : ( A B : ZFSet ) → Set m 51 _∈_ : ( A B : ZFSet ) → Set m
52 A ∈ B = B ∋ A 52 A ∈ B = B ∋ A
53 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 53 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
54 _⊆_ A B {x} = A ∋ x → B ∋ x 54 _⊆_ A B {x} = A ∋ x → B ∋ x
55 _∩_ : ( A B : ZFSet ) → ZFSet 55 _∩_ : ( A B : ZFSet ) → ZFSet
56 A ∩ B = Select A ( λ x d → ( A ∋ x ) ∧ ( B ∋ x ) ) 56 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
57 _∪_ : ( A B : ZFSet ) → ZFSet 57 _∪_ : ( A B : ZFSet ) → ZFSet
58 A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easer 58 A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easer
59 ｛_｝ : ZFSet → ZFSet 59 ｛_｝ : ZFSet → ZFSet
60 ｛ x ｝ = ( x , x ) 60 ｛ x ｝ = ( x , x )
61 infixr 200 _∈_ 61 infixr 200 _∈_
72 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 72 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
73 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) 73 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
74 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 74 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
75 infinity∅ : ∅ ∈ infinite 75 infinity∅ : ∅ ∈ infinite
76 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite 76 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
77 selection : ∀ { X : ZFSet } → { ψ : (x : ZFSet ) → x ∈ X → Set m } → ∀ { y : ZFSet } → ( ( d : y ∈ X ) → ψ y d ) ⇔ (y ∈ Select X ψ ) 77 selection : ∀ { X : ZFSet } → { ψ : (x : ZFSet ) → Set m } → ∀ { y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
78 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 78 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
79 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ ) 79 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
80 -- -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ] 80 -- -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
81 -- axiom-of-choice : Set (suc n) 81 -- axiom-of-choice : Set (suc n)
82 -- axiom-of-choice = ? 82 -- axiom-of-choice = ?
92 -- ZF Set constructor 92 -- ZF Set constructor
93 ∅ : ZFSet 93 ∅ : ZFSet
94 _,_ : ( A B : ZFSet ) → ZFSet 94 _,_ : ( A B : ZFSet ) → ZFSet
95 Union : ( A : ZFSet ) → ZFSet 95 Union : ( A : ZFSet ) → ZFSet
96 Power : ( A : ZFSet ) → ZFSet 96 Power : ( A : ZFSet ) → ZFSet
97 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → X ∋ x → Set m ) → ZFSet 97 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
98 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet 98 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
99 infinite : ZFSet 99 infinite : ZFSet
100 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite 100 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
101 101