Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison zf.agda @ 6:d9b704508281
isEquiv and isZF
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 11 May 2019 11:40:31 +0900 |
parents | c12d964a04c0 |
children | 813f1b3b000b |
comparison
equal
deleted
inserted
replaced
4:c12d964a04c0 | 6:d9b704508281 |
---|---|
13 | 13 |
14 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where | 14 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where |
15 case1 : A → A ∨ B | 15 case1 : A → A ∨ B |
16 case2 : B → A ∨ B | 16 case2 : B → A ∨ B |
17 | 17 |
18 open import Relation.Binary.PropositionalEquality | 18 -- open import Relation.Binary.PropositionalEquality |
19 | 19 |
20 _⇔_ : {n : Level } → ( A B : Set n ) → Set n | 20 _⇔_ : {n : Level } → ( A B : Set n ) → Set n |
21 _⇔_ A B = ( A → B ) ∧ ( B → A ) | 21 _⇔_ A B = ( A → B ) ∧ ( B → A ) |
22 | |
23 open import Data.Empty | |
24 open import Relation.Nullary | |
25 | |
26 open import Relation.Binary | |
27 open import Relation.Binary.Core | |
22 | 28 |
23 infixr 130 _∧_ | 29 infixr 130 _∧_ |
24 infixr 140 _∨_ | 30 infixr 140 _∨_ |
25 infixr 150 _⇔_ | 31 infixr 150 _⇔_ |
26 | 32 |
27 open import Data.Empty | 33 record IsZF {n m : Level } |
28 open import Relation.Nullary | 34 (ZFSet : Set n) |
29 | 35 (_∋_ : ( A x : ZFSet ) → Set m) |
30 record ZF (n m : Level ) : Set (suc (n ⊔ m)) where | 36 (_≈_ : ( A B : ZFSet ) → Set m) |
31 coinductive | 37 (∅ : ZFSet) |
38 (_×_ : ( A B : ZFSet ) → ZFSet) | |
39 (Union : ( A : ZFSet ) → ZFSet) | |
40 (Power : ( A : ZFSet ) → ZFSet) | |
41 (Restrict : ( ZFSet → Set m ) → ZFSet) | |
42 (infinite : ZFSet) | |
43 : Set (suc (n ⊔ m)) where | |
32 field | 44 field |
33 ZFSet : Set n | 45 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ |
34 _∋_ : ( A x : ZFSet ) → Set m | |
35 _≈_ : ( A B : ZFSet ) → Set m | |
36 -- ZF Set constructor | |
37 ∅ : ZFSet | |
38 _×_ : ( A B : ZFSet ) → ZFSet | |
39 Union : ( A : ZFSet ) → ZFSet | |
40 Power : ( A : ZFSet ) → ZFSet | |
41 Restrict : ( ZFSet → Set m ) → ZFSet | |
42 infixl 200 _∋_ | |
43 infixr 210 _×_ | |
44 infixr 220 _≈_ | |
45 field | |
46 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) | 46 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) |
47 pair : ( A B : ZFSet ) → A × B ∋ A ∧ A × B ∋ B | 47 pair : ( A B : ZFSet ) → ( (A × B) ∋ A ) ∧ ( (A × B) ∋ B ) |
48 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x)) | 48 -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x)) |
49 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y | 49 union→ : ( X x y : ZFSet ) → X ∋ x → x ∋ y → Union X ∋ y |
50 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y | 50 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y |
51 _∈_ : ( A B : ZFSet ) → Set m | 51 _∈_ : ( A B : ZFSet ) → Set m |
52 A ∈ B = B ∋ A | 52 A ∈ B = B ∋ A |
63 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) | 63 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) |
64 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) | 64 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) |
65 power→ : ( A t : ZFSet ) → Power A ∋ t → ∀ {x} {y} → _⊆_ t A {x} {y} | 65 power→ : ( A t : ZFSet ) → Power A ∋ t → ∀ {x} {y} → _⊆_ t A {x} {y} |
66 power← : ( A t : ZFSet ) → ∀ {x} {y} → _⊆_ t A {x} {y} → Power A ∋ t | 66 power← : ( A t : ZFSet ) → ∀ {x} {y} → _⊆_ t A {x} {y} → Power A ∋ t |
67 -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) | 67 -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) |
68 extentionality : ( A B z : ZFSet ) → A ∋ z ⇔ B ∋ z → A ≈ B | 68 extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B |
69 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) | 69 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) |
70 -- smaller : ZFSet → ZFSet | 70 -- smaller : ZFSet → ZFSet |
71 -- regularity : ( x : ZFSet ) → ¬ (x ≈ ∅) → smaller x ∩ x ≈ ∅ | 71 -- regularity : ( x : ZFSet ) → ¬ (x ≈ ∅) → smaller x ∩ x ≈ ∅ |
72 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) | 72 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) |
73 infinite : ZFSet | |
74 infinity∅ : ∅ ∈ infinite | 73 infinity∅ : ∅ ∈ infinite |
75 infinity : ( x : ZFSet ) → x ∈ infinite → ( x ∪ Restrict ( λ y → x ≈ y )) ∈ infinite | 74 infinity : ( x : ZFSet ) → x ∈ infinite → ( x ∪ Restrict ( λ y → x ≈ y )) ∈ infinite |
76 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) | 75 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) |
77 replacement : ( ψ : ZFSet → Set m ) → ( y : ZFSet ) → y ∈ Restrict ψ → ψ y | 76 replacement : ( ψ : ZFSet → Set m ) → ( y : ZFSet ) → y ∈ Restrict ψ → ψ y |
78 | 77 |
78 record ZF {n m : Level } : Set (suc (n ⊔ m)) where | |
79 coinductive | |
80 infixr 210 _×_ | |
81 infixl 200 _∋_ | |
82 infixr 220 _≈_ | |
83 field | |
84 ZFSet : Set n | |
85 _∋_ : ( A x : ZFSet ) → Set m | |
86 _≈_ : ( A B : ZFSet ) → Set m | |
87 -- ZF Set constructor | |
88 ∅ : ZFSet | |
89 _×_ : ( A B : ZFSet ) → ZFSet | |
90 Union : ( A : ZFSet ) → ZFSet | |
91 Power : ( A : ZFSet ) → ZFSet | |
92 Restrict : ( ZFSet → Set m ) → ZFSet | |
93 infinite : ZFSet | |
94 field | |
95 isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Restrict infinite | |
96 |