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

comparison zf.agda @ 103:c8b79d303867

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
starting over HOD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Jun 2019 10:45:00 +0900
parents 9a7a64b2388c
children 1daa1d24348c
comparison
equal deleted inserted replaced
101:52a82415dfc8 103:c8b79d303867
18 _⇔_ : {n : Level } → ( A B : Set n ) → Set n 18 _⇔_ : {n : Level } → ( A B : Set n ) → Set n
19 _⇔_ A B = ( A → B ) ∧ ( B → A ) 19 _⇔_ A B = ( A → B ) ∧ ( B → A )
20 20
21 open import Relation.Nullary 21 open import Relation.Nullary
22 open import Relation.Binary 22 open import Relation.Binary
23
24 contra-position : {n : Level } {A B : Set n} → (A → B) → ¬ B → ¬ A
25 contra-position {n} {A} {B} f ¬b a = ¬b ( f a )
23 26
24 infixr 130 _∧_ 27 infixr 130 _∧_
25 infixr 140 _∨_ 28 infixr 140 _∨_
26 infixr 150 _⇔_ 29 infixr 150 _⇔_
27 30
50 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 53 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
51 _⊆_ A B {x} = A ∋ x → B ∋ x 54 _⊆_ A B {x} = A ∋ x → B ∋ x
52 _∩_ : ( A B : ZFSet ) → ZFSet 55 _∩_ : ( A B : ZFSet ) → ZFSet
53 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) 56 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
54 _∪_ : ( A B : ZFSet ) → ZFSet 57 _∪_ : ( A B : ZFSet ) → ZFSet
55 A ∪ B = Union (A , B) 58 A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easer
56 ｛_｝ : ZFSet → ZFSet 59 ｛_｝ : ZFSet → ZFSet
57 ｛ x ｝ = ( x , x ) 60 ｛ x ｝ = ( x , x )
58 infixr 200 _∈_ 61 infixr 200 _∈_
59 infixr 230 _∩_ _∪_ 62 infixr 230 _∩_ _∪_
60 infixr 220 _⊆_ 63 infixr 220 _⊆_
72 infinity∅ : ∅ ∈ infinite 75 infinity∅ : ∅ ∈ infinite
73 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite 76 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
74 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) 77 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
75 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 78 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
76 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ ) 79 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
80 -- -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
81 -- axiom-of-choice : Set (suc n)
82 -- axiom-of-choice = ?
77 83
78 record ZF {n m : Level } : Set (suc (n ⊔ m)) where 84 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
79 infixr 210 _,_ 85 infixr 210 _,_
80 infixl 200 _∋_ 86 infixl 200 _∋_
81 infixr 220 _≈_ 87 infixr 220 _≈_