Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate zfc.agda @ 276:6f10c47e4e7a
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 |
| rev | line source |
|---|---|
| 276 | 1 module zfc where |
| 3 | 2 |
| 3 open import Level | |
| 276 | 4 open import Relation.Binary |
| 5 open import Relation.Nullary | |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
209
diff
changeset
|
6 open import logic |
| 123 | 7 |
| 276 | 8 record IsZFC {n m : Level } |
| 6 | 9 (ZFSet : Set n) |
| 10 (_∋_ : ( A x : ZFSet ) → Set m) | |
|
9
5ed16e2d8eb7
try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
11 (_≈_ : Rel ZFSet m) |
| 6 | 12 (∅ : ZFSet) |
| 115 | 13 (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) |
| 274 | 14 : Set (suc (n ⊔ suc m)) where |
| 3 | 15 field |
| 276 | 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 _∩_ | |
| 3 | 21 _∈_ : ( A B : ZFSet ) → Set m |
| 22 A ∈ B = B ∋ A | |
| 23 _∩_ : ( A B : ZFSet ) → ZFSet | |
| 115 | 24 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) |
| 3 | 25 |
| 276 | 26 record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where |
| 6 | 27 field |
| 28 ZFSet : Set n | |
| 29 _∋_ : ( A x : ZFSet ) → Set m | |
| 30 _≈_ : ( A B : ZFSet ) → Set m | |
| 31 ∅ : ZFSet | |
| 115 | 32 Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet |
| 276 | 33 isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select |
| 6 | 34 |