annotate zf.agda @ 72:f39f1a90d154

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jun 2019 14:43:05 +0900
parents cd9cf8b09610
children dd430a95610f
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module zf where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
5 data Bool : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
6 true : Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
7 false : Bool
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 field
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 proj1 : A
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 proj2 : B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open _∧_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 case1 : A → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 case2 : B → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
21 -- open import Relation.Binary.PropositionalEquality
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 _⇔_ : {n : Level } → ( A B : Set n ) → Set n
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 _⇔_ A B = ( A → B ) ∧ ( B → A )
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
26 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
27 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
28
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
29 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
30 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
31
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 infixr 130 _∧_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 infixr 140 _∨_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 infixr 150 _⇔_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
36 record IsZF {n m : Level }
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
37 (ZFSet : Set n)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
38 (_∋_ : ( A x : ZFSet ) → Set m)
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
39 (_≈_ : Rel ZFSet m)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
40 (∅ : ZFSet)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
41 (_,_ : ( A B : ZFSet ) → ZFSet)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
42 (Union : ( A : ZFSet ) → ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
43 (Power : ( A : ZFSet ) → ZFSet)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
44 (Select : ZFSet → ( ZFSet → Set m ) → ZFSet )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
45 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
46 (infinite : ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
47 : Set (suc (n ⊔ m)) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 field
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
49 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
51 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B )
69
93abc0133b8a union continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
52 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
70
cd9cf8b09610 Union needs +1 space
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
53 union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet
cd9cf8b09610 Union needs +1 space
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
54 union→ : ( X z u : ZFSet ) → ((Union X ∋ u ) ∧ (u ∋ z )) → Union X ∋ z
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
55 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 _∈_ : ( A B : ZFSet ) → Set m
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 A ∈ B = B ∋ A
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
58 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
59 _⊆_ A B {x} = A ∋ x → B ∋ x
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 _∩_ : ( A B : ZFSet ) → ZFSet
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
61 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 _∪_ : ( A B : ZFSet ) → ZFSet
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
63 A ∪ B = Union (A , B)
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 infixr 200 _∈_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 infixr 230 _∩_ _∪_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 infixr 220 _⊆_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 field
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
68 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
70 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
71 power← : ∀( A t : ZFSet ) → ∀ {x} → _⊆_ t A {x} → Power A ∋ t
65
164ad5a703d8 ¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
72 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
69
93abc0133b8a union continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
73 extensionality : { A B z : ZFSet } → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
37
f10ceee99d00 ¬ ( y c< x ) → x ≡ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
75 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
f10ceee99d00 ¬ ( y c< x ) → x ≡ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
76 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 infinity∅ : ∅ ∈ infinite
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
79 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ Select X ( λ y → x ≈ y )) ∈ infinite
54
33fb8228ace9 fix selection axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
80 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
82 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
84 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
85 infixr 210 _,_
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
86 infixl 200 _∋_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
87 infixr 220 _≈_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
88 field
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
89 ZFSet : Set n
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
90 _∋_ : ( A x : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
91 _≈_ : ( A B : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
92 -- ZF Set constructor
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
93 ∅ : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
94 _,_ : ( A B : ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
95 Union : ( A : ZFSet ) → ZFSet
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
96 Power : ( A : ZFSet ) → ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
97 Select : ZFSet → ( ZFSet → Set m ) → ZFSet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
98 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
99 infinite : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
100 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
101
10
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
102 module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
103
10
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
104 _≈_ = ZF._≈_ zf
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
105 ZFSet = ZF.ZFSet zf
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
106 Select = ZF.Select zf
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
107 ∅ = ZF.∅ zf
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
108 _∩_ = ( IsZF._∩_ ) (ZF.isZF zf)
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
109 _∋_ = ZF._∋_ zf
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
110 replacement = IsZF.replacement ( ZF.isZF zf )
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
111 selection = IsZF.selection ( ZF.isZF zf )
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
112 minimul = IsZF.minimul ( ZF.isZF zf )
8022e14fce74 add constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
113 regularity = IsZF.regularity ( ZF.isZF zf )
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
114
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
115 -- russel : Select ( λ x → x ∋ x ) ≈ ∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
116 -- russel with Select ( λ x → x ∋ x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
117 -- ... | s = {!!}
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
118