|
1097
|
1 open import Level
|
|
|
2 module NSet (n : Level) where
|
|
|
3
|
|
|
4 open import logic
|
|
|
5 open import nat
|
|
|
6 open import Data.Nat hiding (suc ; zero)
|
|
|
7 open import Data.Nat.Properties
|
|
|
8 open import Relation.Binary hiding (_⇔_)
|
|
|
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
10
|
|
|
11 --
|
|
|
12 -- Primitive Set on ℕ
|
|
|
13 --
|
|
|
14
|
|
|
15 record NSet : Set (suc zero) where
|
|
|
16 field
|
|
|
17 def : ℕ → Set
|
|
|
18
|
|
|
19 --
|
|
|
20 -- Set as an equation on ℕ
|
|
|
21 --
|
|
|
22 eqa1 : NSet
|
|
|
23 eqa1 = record { def = λ x → x * x + 6 ≡ 5 * x }
|
|
|
24
|
|
|
25 open NSet
|
|
|
26
|
|
|
27 _∋_ : NSet → ℕ → Set
|
|
|
28 S ∋ x = def S x
|
|
|
29
|
|
|
30 eq1∋2 : eqa1 ∋ 2
|
|
|
31 eq1∋2 = refl
|
|
|
32
|
|
|
33 eq1∋3 : eqa1 ∋ 3
|
|
|
34 eq1∋3 = refl
|
|
|
35
|
|
|
36 --
|
|
|
37 -- The solution
|
|
|
38 --
|
|
|
39
|
|
|
40 eqa2 : NSet
|
|
|
41 eqa2 = record { def = λ x → (x ≡ 2) ∨ ( x ≡ 3 ) }
|
|
|
42
|
|
|
43 eq2∋3 : eqa2 ∋ 3
|
|
|
44 eq2∋3 = case2 refl
|
|
|
45
|
|
|
46 record _==_ ( a b : NSet ) : Set where
|
|
|
47 field
|
|
|
48 eq→ : ∀ { x : ℕ } → def a x → def b x
|
|
|
49 eq← : ∀ { x : ℕ } → def b x → def a x
|
|
|
50
|
|
|
51 _⊆_ : (a b : NSet ) → Set
|
|
|
52 _⊆_ a b = ∀ {x : ℕ} → def a x → def b x
|
|
|
53
|
|
|
54 eq2⊆eq1 : eqa2 ⊆ eqa1
|
|
|
55 eq2⊆eq1 {2} (case1 refl) = refl
|
|
|
56 eq2⊆eq1 {3} (case2 refl) = refl
|
|
|
57
|
|
|
58 -- the other way is slightly difficut
|
|
|
59
|
|
|
60 data ⊥ : Set where
|
|
|
61
|
|
|
62 ⊥-elim : {A : Set } → ⊥ → A
|
|
|
63 ⊥-elim ()
|
|
|
64
|
|
|
65 ¬_ : Set → Set
|
|
|
66 ¬ A = A → ⊥
|
|
|
67
|
|
|
68 n∅ : NSet
|
|
|
69 n∅ = record { def = λ y → y < 0 }
|
|
|
70
|
|
|
71 ¬n∅∋x : {x : ℕ } → ¬ ( n∅ ∋ x )
|
|
|
72 ¬n∅∋x ()
|
|
|
73
|
|
|
74 ¬n∅∋x' : {x : ℕ } → ¬ ( n∅ ∋ x )
|
|
|
75 ¬n∅∋x' {x} nx = ⊥-elim ( n1 nx ) where
|
|
|
76 n1 : x < 0 → ⊥
|
|
|
77 n1 ()
|
|
|
78
|
|
|
79 --
|
|
|
80 -- Set of subset of ℕ
|
|
|
81 --
|
|
|
82
|
|
|
83 record NSetSet : Set (suc zero) where
|
|
|
84 field
|
|
|
85 ndef : NSet → Set
|
|
|
86
|
|
|
87 open NSetSet
|
|
|
88
|
|
|
89 record _=n=_ ( a b : NSetSet ) : Set (suc zero) where
|
|
|
90 field
|
|
|
91 eq→ : ∀ { x : NSet } → ndef a x → ndef b x
|
|
|
92 eq← : ∀ { x : NSet } → ndef b x → ndef a x
|
|
|
93
|
|
|
94 eqa3 : NSetSet
|
|
|
95 eqa3 = record { ndef = λ x → x == eqa2 }
|
|
|
96
|
|
|
97 --
|
|
|
98 -- Can we defined hierarchy of Set in monothic and consitent way?
|
|
|
99 -- equations on Ordinal is an solution (Ordinal Definable Set)
|
|
|
100 -- but we need some axioms to achive ZF Set Theory
|
|
|
101 --
|
|
|
102
|
|
|
103
|
|
|
104
|
|
|
105
|
