|
431
|
1 module zfc where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Relation.Binary
|
|
|
5 open import Relation.Nullary
|
|
|
6 open import logic
|
|
|
7
|
|
|
8 record IsZFC {n m : Level }
|
|
|
9 (ZFSet : Set n)
|
|
|
10 (_∋_ : ( A x : ZFSet ) → Set m)
|
|
|
11 (_≈_ : Rel ZFSet m)
|
|
|
12 (∅ : ZFSet)
|
|
|
13 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
|
|
|
14 : Set (suc (n ⊔ suc m)) where
|
|
|
15 field
|
|
|
16 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
17 choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
|
|
|
18 choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
|
|
|
19 infixr 200 _∈_
|
|
|
20 infixr 230 _∩_
|
|
|
21 _∈_ : ( A B : ZFSet ) → Set m
|
|
|
22 A ∈ B = B ∋ A
|
|
|
23 _∩_ : ( A B : ZFSet ) → ZFSet
|
|
|
24 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
|
|
|
25
|
|
|
26 record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where
|
|
|
27 field
|
|
|
28 ZFSet : Set n
|
|
|
29 _∋_ : ( A x : ZFSet ) → Set m
|
|
|
30 _≈_ : ( A B : ZFSet ) → Set m
|
|
|
31 ∅ : ZFSet
|
|
|
32 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
|
|
|
33 isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select
|
|
|
34
|
