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

comparison zf.agda @ 376:6c72bee25653

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Jul 2020 16:28:12 +0900
parents 8cade5f660bd
children cc7909f86841
comparison
equal deleted inserted replaced
375:8cade5f660bd 376:6c72bee25653
14 (_≈_ : Rel ZFSet m) 14 (_≈_ : Rel ZFSet m)
15 (∅ : ZFSet) 15 (∅ : ZFSet)
16 (_,_ : ( A B : ZFSet ) → ZFSet) 16 (_,_ : ( A B : ZFSet ) → ZFSet)
17 (Union : ( A : ZFSet ) → ZFSet) 17 (Union : ( A : ZFSet ) → ZFSet)
18 (Power : ( A : ZFSet ) → ZFSet) 18 (Power : ( A : ZFSet ) → ZFSet)
19 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → (X ∋ x) → Set m ) → ZFSet ) 19 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
20 (Replace : (X : ZFSet) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet ) 20 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
21 (infinite : ZFSet) 21 (infinite : ZFSet)
22 : Set (suc (n ⊔ suc m)) where 22 : Set (suc (n ⊔ suc m)) where
23 field 23 field
24 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 24 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
25 -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t ≈ y) 25 -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t ≈ y)
31 _∈_ : ( A B : ZFSet ) → Set m 31 _∈_ : ( A B : ZFSet ) → Set m
32 A ∈ B = B ∋ A 32 A ∈ B = B ∋ A
33 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 33 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
34 _⊆_ A B {x} = A ∋ x → B ∋ x 34 _⊆_ A B {x} = A ∋ x → B ∋ x
35 _∩_ : ( A B : ZFSet ) → ZFSet 35 _∩_ : ( A B : ZFSet ) → ZFSet
36 A ∩ B = Select A ( λ x _ → ( A ∋ x ) ∧ ( B ∋ x ) ) 36 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
37 _∪_ : ( A B : ZFSet ) → ZFSet 37 _∪_ : ( A B : ZFSet ) → ZFSet
38 A ∪ B = Union (A , B) 38 A ∪ B = Union (A , B)
39 ｛_｝ : ZFSet → ZFSet 39 ｛_｝ : ZFSet → ZFSet
40 ｛ x ｝ = ( x , x ) 40 ｛ x ｝ = ( x , x )
41 infixr 200 _∈_ 41 infixr 200 _∈_
53 → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) 53 → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x )
54 → (x : ZFSet ) → ψ x 54 → (x : ZFSet ) → ψ x
55 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 55 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
56 infinity∅ : ∅ ∈ infinite 56 infinity∅ : ∅ ∈ infinite
57 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite 57 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
58 selection : ∀ { X y : ZFSet } → { ψ : (x : ZFSet ) → X ∋ x → Set m } → (y ∈ X ∧ (( y∈X : y ∈ X ) → ψ y y∈X)) ⇔ (y ∈ Select X ψ ) 58 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
59 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 59 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
60 replacement← : ∀ ( X x : ZFSet ) → (x∈X : x ∈ X ) → {ψ : (x : ZFSet ) → x ∈ X → ZFSet} → ψ x x∈X ∈ Replace X ψ 60 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
61 replacement→ : ∀ ( X x : ZFSet ) → {ψ : (x : ZFSet ) → X ∋ x → ZFSet} → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → (X∋y : X ∋ y ) → ¬ ( x ≈ ψ y X∋y ) ) 61 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
62 62
63 record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where 63 record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
64 infixr 210 _,_ 64 infixr 210 _,_
65 infixl 200 _∋_ 65 infixl 200 _∋_
66 infixr 220 _≈_ 66 infixr 220 _≈_
71 -- ZF Set constructor 71 -- ZF Set constructor
72 ∅ : ZFSet 72 ∅ : ZFSet
73 _,_ : ( A B : ZFSet ) → ZFSet 73 _,_ : ( A B : ZFSet ) → ZFSet
74 Union : ( A : ZFSet ) → ZFSet 74 Union : ( A : ZFSet ) → ZFSet
75 Power : ( A : ZFSet ) → ZFSet 75 Power : ( A : ZFSet ) → ZFSet
76 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → ( X ∋ x ) → Set m ) → ZFSet 76 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
77 Replace : (X : ZFSet ) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet 77 Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
78 infinite : ZFSet 78 infinite : ZFSet
79 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite 79 isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite
80 80