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

comparison zfc.agda @ 276:6f10c47e4e7a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate choice fix sup-o
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:02:52 +0900
parents zf.agda@29a85a427ed2
children
comparison
equal deleted inserted replaced
275:455792eaa611 276:6f10c47e4e7a
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