|
0
|
1 module set-of-agda where
|
|
|
2
|
|
|
3 open import Level
|
|
2
|
4 open import Data.Bool
|
|
0
|
5
|
|
2
|
6 -- infix 50 _∧_
|
|
|
7
|
|
|
8 -- record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
9 -- constructor _×_
|
|
|
10 -- field
|
|
|
11 -- proj1 : A
|
|
|
12 -- proj2 : B
|
|
|
13
|
|
|
14 -- open _∧_
|
|
0
|
15
|
|
2
|
16 -- infix 50 _∨_
|
|
|
17
|
|
|
18 -- data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
19 -- case1 : A → A ∨ B
|
|
|
20 -- case2 : B → A ∨ B
|
|
0
|
21
|
|
3
|
22 data ZFSet {n : Level} : Set (suc (suc n)) where
|
|
2
|
23 elem : { A : Set n } ( a : A ) → ZFSet
|
|
|
24 ∅ : ZFSet {n}
|
|
|
25 pair : {A B : Set n} (a : A ) (b : B ) → ZFSet
|
|
3
|
26 union : (A : Set (suc n) ) → ZFSet
|
|
|
27 -- repl : ( ψ : ZFSet {n} → Set zero ) → ZFSet
|
|
2
|
28 infinite : ZFSet
|
|
|
29 power : (A : ZFSet {n}) → ZFSet
|
|
0
|
30
|
|
|
31 infix 60 _∋_ _∈_
|
|
|
32
|
|
2
|
33 open import Relation.Binary.PropositionalEquality
|
|
0
|
34
|
|
2
|
35 data _∈_ {n : Level} : {A : Set n} ( a : A ) ( Z : ZFSet {n} ) → Set (suc n) where
|
|
|
36 ∈-elm : {A : Set n } {a : A} → a ∈ (elem a)
|
|
|
37 ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A} → a ∈ (pair a b)
|
|
|
38 ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B} → b ∈ (pair a b)
|
|
3
|
39 -- ∈-union : {Z : Set (suc n)} {A : Z } → {a : {!!} } → a ∈ (union Z)
|
|
|
40 -- ∈-repl : {A : Set n } { B : Set n} → { ψ : B → A } → { b : B } → ψ b ∈ {!!} -- (repl {!!})
|
|
2
|
41 -- ∈-infinite-1 : ∅ ∈ infinite
|
|
|
42 -- ∈-infinite : {A : Set n} {a : A} → _∈_ infinite {A} a
|
|
3
|
43 ∈-power : {A B : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈ (power Z)
|
|
2
|
44
|
|
|
45 -- _∈_ : {n : Level} { A : ZFSet {n} } → {B : Set n} → (a : B ) → Set n → Bool
|
|
|
46 -- _∈_ {_} {A} a _ = A ∋ a
|
|
0
|
47
|
|
|
48 infix 40 _⇔_
|
|
|
49
|
|
2
|
50 -- _⇔_ : {n : Level} (A B : Set n) → Set n
|
|
|
51 -- A ⇔ B = ( ∀ {x : A } → x ∈ B ) ∧ ( ∀ {x : B } → x ∈ A )
|
|
0
|
52
|
|
|
53 -- Axiom of extentionality
|
|
|
54 -- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ]
|
|
|
55
|
|
2
|
56 -- set-extentionality : {n : Level } {x y : Set n } → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n)) → ( x ∈ w ⇔ y ∈ w )
|
|
|
57 -- proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x )
|
|
|
58 -- proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y )
|
|
1
|
59
|
|
|
60
|
|
|
61 open import Relation.Nullary
|
|
|
62 open import Data.Empty
|
|
|
63
|
|
2
|
64 -- data ∅ : Set where
|
|
1
|
65
|
|
|
66 infix 50 _∩_
|
|
0
|
67
|
|
2
|
68 -- record _∩_ {n m : Level} (A : Set n) ( B : Set m) : Set (n ⊔ m) where
|
|
|
69 -- field
|
|
|
70 -- inL : {x : A } → x ∈ A
|
|
|
71 -- inR : {x : B } → x ∈ B
|
|
1
|
72
|
|
2
|
73 -- open _∩_
|
|
1
|
74
|
|
|
75 -- lemma : {n m : Level} (A : Set n) ( B : Set m) → (a : A ) → a ∈ (A ∩ B)
|
|
|
76 -- lemma A B a A∩B = inL A∩B
|
|
|
77
|
|
2
|
78 -- Axiom of regularity
|
|
|
79 -- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
|
|
|
80
|
|
1
|
81 -- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x ⇔ ∅ )
|
|
|
82 -- set-regularity = {!!}
|
|
|
83
|
|
2
|
84 -- Axiom of pairing
|
|
|
85 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z).
|
|
|
86
|
|
|
87 -- pair : {n m : Level} ( x : Set n ) ( y : Set m ) → Set (n ⊔ m)
|
|
|
88 -- pair x y = {!!} -- ( x × y )
|
|
|
89
|
|
|
90 -- Axiom of Union
|
|
|
91 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x))
|
|
|
92
|
|
|
93 -- axiom of infinity
|
|
|
94 -- ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
|
|
|
95
|
|
|
96 -- axiom of replacement
|
|
|
97 -- ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
|
|
|
98
|
|
|
99 -- axiom of power set
|
|
|
100 -- ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
|
|
|
101
|
|
|
102
|
|
|
103
|
|
|
104
|
