Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison zf.agda @ 18:627a79e61116

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 May 2019 10:55:34 +0900
parents e11e95d5ddee
children 7293a151d949
comparison
equal deleted inserted replaced
17:6a668c6086a5 18:627a79e61116
42 record IsZF {n m : Level } 42 record IsZF {n m : Level }
43 (ZFSet : Set n) 43 (ZFSet : Set n)
44 (_∋_ : ( A x : ZFSet ) → Set m) 44 (_∋_ : ( A x : ZFSet ) → Set m)
45 (_≈_ : Rel ZFSet m) 45 (_≈_ : Rel ZFSet m)
46 (∅ : ZFSet) 46 (∅ : ZFSet)
47 (_×_ : ( A B : ZFSet ) → ZFSet) 47 (_,_ : ( A B : ZFSet ) → ZFSet)
48 (Union : ( A : ZFSet ) → ZFSet) 48 (Union : ( A : ZFSet ) → ZFSet)
49 (Power : ( A : ZFSet ) → ZFSet) 49 (Power : ( A : ZFSet ) → ZFSet)
50 (Select : ( ZFSet → Set m ) → ZFSet ) 50 (Select : ZFSet → ( ZFSet → Set m ) → ZFSet )
51 (Replace : ( ZFSet → ZFSet ) → ZFSet ) 51 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
52 (infinite : ZFSet) 52 (infinite : ZFSet)
53 : Set (suc (n ⊔ m)) where 53 : Set (suc (n ⊔ m)) where
54 field 54 field
55 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ 55 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_
56 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) 56 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
57 pair : ( A B : ZFSet ) → ( (A × B) ∋ A ) ∧ ( (A × B) ∋ B ) 57 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B )
58 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x)) 58 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x))
59 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y 59 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y
60 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y 60 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y
61 _∈_ : ( A B : ZFSet ) → Set m 61 _∈_ : ( A B : ZFSet ) → Set m
62 A ∈ B = B ∋ A 62 A ∈ B = B ∋ A
63 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m 63 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
64 _⊆_ A B {x} {A∋x} = B ∋ x 64 _⊆_ A B {x} {A∋x} = B ∋ x
65 _∩_ : ( A B : ZFSet ) → ZFSet 65 _∩_ : ( A B : ZFSet ) → ZFSet
66 A ∩ B = Select ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) 66 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
67 _∪_ : ( A B : ZFSet ) → ZFSet 67 _∪_ : ( A B : ZFSet ) → ZFSet
68 A ∪ B = Select ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) 68 A ∪ B = Select (A , B) ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) )
69 infixr 200 _∈_ 69 infixr 200 _∈_
70 infixr 230 _∩_ _∪_ 70 infixr 230 _∩_ _∪_
71 infixr 220 _⊆_ 71 infixr 220 _⊆_
72 field 72 field
73 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 73 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
79 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 79 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
80 minimul : ZFSet → ZFSet 80 minimul : ZFSet → ZFSet
81 regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( minimul x ∈ x ∧ ( minimul x ∩ x ≈ ∅ ) ) 81 regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( minimul x ∈ x ∧ ( minimul x ∩ x ≈ ∅ ) )
82 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 82 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
83 infinity∅ : ∅ ∈ infinite 83 infinity∅ : ∅ ∈ infinite
84 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ Select ( λ y → x ≈ y )) ∈ infinite 84 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ Select X ( λ y → x ≈ y )) ∈ infinite
85 selection : { ψ : ZFSet → Set m } → ∀ ( y : ZFSet ) → ( y ∈ Select ψ ) → ψ y 85 selection : { ψ : ZFSet → Set m } → ∀ ( X y : ZFSet ) → ( y ∈ Select X ψ ) → ψ y
86 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 86 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
87 replacement : {ψ : ZFSet → ZFSet} → ∀ ( x : ZFSet ) → ( ψ x ∈ Replace ψ ) 87 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
88 88
89 record ZF {n m : Level } : Set (suc (n ⊔ m)) where 89 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
90 infixr 210 _×_ 90 infixr 210 _,_
91 infixl 200 _∋_ 91 infixl 200 _∋_
92 infixr 220 _≈_ 92 infixr 220 _≈_
93 field 93 field
94 ZFSet : Set n 94 ZFSet : Set n
95 _∋_ : ( A x : ZFSet ) → Set m 95 _∋_ : ( A x : ZFSet ) → Set m
96 _≈_ : ( A B : ZFSet ) → Set m 96 _≈_ : ( A B : ZFSet ) → Set m
97 -- ZF Set constructor 97 -- ZF Set constructor
98 ∅ : ZFSet 98 ∅ : ZFSet
99 _×_ : ( A B : ZFSet ) → ZFSet 99 _,_ : ( A B : ZFSet ) → ZFSet
100 Union : ( A : ZFSet ) → ZFSet 100 Union : ( A : ZFSet ) → ZFSet
101 Power : ( A : ZFSet ) → ZFSet 101 Power : ( A : ZFSet ) → ZFSet
102 Select : ( ZFSet → Set m ) → ZFSet 102 Select : ZFSet → ( ZFSet → Set m ) → ZFSet
103 Replace : ( ZFSet → ZFSet ) → ZFSet 103 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
104 infinite : ZFSet 104 infinite : ZFSet
105 isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Select Replace infinite 105 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
106 106
107 module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where 107 module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where
108 108
109 _≈_ = ZF._≈_ zf 109 _≈_ = ZF._≈_ zf
110 ZFSet = ZF.ZFSet zf 110 ZFSet = ZF.ZFSet zf