annotate zf.agda @ 140:312e27aa3cb5

remove otrans again. start over
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 23:02:47 +0900
parents 567084f2278f
children 3675bd617ac8
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 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
15 case1 : A → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 case2 : B → A ∨ B
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
116
47541e86c6ac axiom of selection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
18 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
77
75ba8cf64707 Power Set on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
19 _⇔_ A B = ( A → B ) ∧ ( B → A )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
21
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
22 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
23 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
24
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 133
diff changeset
25 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 133
diff changeset
26 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
103
c8b79d303867 starting over HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
27
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 infixr 130 _∧_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 infixr 140 _∨_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 infixr 150 _⇔_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
32 record IsZF {n m : Level }
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
33 (ZFSet : Set n)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
34 (_∋_ : ( 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
35 (_≈_ : Rel ZFSet m)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
36 (∅ : ZFSet)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
37 (_,_ : ( A B : ZFSet ) → ZFSet)
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
38 (Union : ( A : ZFSet ) → ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
39 (Power : ( A : ZFSet ) → ZFSet)
115
277c2f3b8acb Select declaration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
40 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
41 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
42 (infinite : ZFSet)
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
43 : Set (suc (n ⊔ m)) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 field
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
45 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
47 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
48 -- ∀ 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
49 union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet
73
dd430a95610f fix ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
50 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
51 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
52 _∈_ : ( A B : ZFSet ) → Set m
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 A ∈ B = B ∋ A
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
54 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
55 _⊆_ A B {x} = A ∋ x → B ∋ x
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 _∩_ : ( A B : ZFSet ) → ZFSet
115
277c2f3b8acb Select declaration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
57 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 _∪_ : ( A B : ZFSet ) → ZFSet
103
c8b79d303867 starting over HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
59 A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easer
78
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
60 {_} : ZFSet → ZFSet
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
61 { x } = ( x , x )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 infixr 200 _∈_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 infixr 230 _∩_ _∪_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 infixr 220 _⊆_
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 field
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
66 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
68 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x}
77
75ba8cf64707 Power Set on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
69 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
70 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
76
8e8f54e7a030 extensionality done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
71 extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 -- 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
73 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
f10ceee99d00 ¬ ( y c< x ) → x ≡ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
74 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
75 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 infinity∅ : ∅ ∈ infinite
78
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
77 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ { x }) ∈ infinite
140
312e27aa3cb5 remove otrans again. start over
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
78 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
79 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
130
3849614bef18 new replacement axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
80 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 133
diff changeset
81 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
103
c8b79d303867 starting over HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
82 -- -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ { t }) ]
c8b79d303867 starting over HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
83 -- axiom-of-choice : Set (suc n)
c8b79d303867 starting over HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
84 -- axiom-of-choice = ?
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
86 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
87 infixr 210 _,_
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
88 infixl 200 _∋_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
89 infixr 220 _≈_
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
90 field
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
91 ZFSet : Set n
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
92 _∋_ : ( A x : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
93 _≈_ : ( A B : ZFSet ) → Set m
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
94 -- ZF Set constructor
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
95 ∅ : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
96 _,_ : ( A B : ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
97 Union : ( A : ZFSet ) → ZFSet
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
98 Power : ( A : ZFSet ) → ZFSet
115
277c2f3b8acb Select declaration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
99 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
100 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
101 infinite : ZFSet
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
102 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
103