|
0
|
1 module set-of-agda where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4
|
|
|
5 infix 50 _∧_
|
|
|
6
|
|
|
7 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
8 constructor _×_
|
|
|
9 field
|
|
|
10 proj1 : A
|
|
|
11 proj2 : B
|
|
|
12
|
|
|
13 open _∧_
|
|
|
14
|
|
|
15 infix 50 _∨_
|
|
|
16
|
|
|
17 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
18 case1 : A → A ∨ B
|
|
|
19 case2 : B → A ∨ B
|
|
|
20
|
|
|
21 infix 60 _∋_ _∈_
|
|
|
22
|
|
1
|
23 data _∋_ {n : Level} ( A : Set n ) : (a : A ) → Set n where
|
|
|
24 elem : (a : A) → A ∋ a
|
|
0
|
25
|
|
1
|
26 _∈_ : {n : Level} { A : Set n } → (a : A ) → Set n → Set n
|
|
|
27 _∈_ {_} {A} a _ = A ∋ a
|
|
0
|
28
|
|
|
29 infix 40 _⇔_
|
|
|
30
|
|
|
31 _⇔_ : {n : Level} (A B : Set n) → Set n
|
|
|
32 A ⇔ B = ( ∀ {x : A } → x ∈ B ) ∧ ( ∀ {x : B } → x ∈ A )
|
|
|
33
|
|
|
34 -- Axiom of extentionality
|
|
|
35 -- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ]
|
|
|
36
|
|
|
37 set-extentionality : {n : Level } {x y : Set n } → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n)) → ( x ∈ w ⇔ y ∈ w )
|
|
1
|
38 proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x )
|
|
|
39 proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y )
|
|
|
40
|
|
|
41 -- Axiom of regularity
|
|
|
42 -- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
|
|
|
43
|
|
|
44 open import Relation.Nullary
|
|
|
45 open import Data.Empty
|
|
|
46
|
|
|
47 data ∅ : Set where
|
|
|
48
|
|
|
49 infix 50 _∩_
|
|
0
|
50
|
|
1
|
51 record _∩_ {n m : Level} (A : Set n) ( B : Set m) : Set (n ⊔ m) where
|
|
|
52 field
|
|
|
53 inL : {x : A } → x ∈ A
|
|
|
54 inR : {x : B } → x ∈ B
|
|
|
55
|
|
|
56 open _∩_
|
|
|
57
|
|
|
58 -- lemma : {n m : Level} (A : Set n) ( B : Set m) → (a : A ) → a ∈ (A ∩ B)
|
|
|
59 -- lemma A B a A∩B = inL A∩B
|
|
|
60
|
|
|
61 -- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x ⇔ ∅ )
|
|
|
62 -- set-regularity = {!!}
|
|
|
63
|
