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

comparison set-of-agda.agda @ 3:e7990ff544bf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reocrd ZF
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 May 2019 10:47:23 +0900
parents 5c819f837721
children
comparison
equal deleted inserted replaced
2:5c819f837721 3:e7990ff544bf
17 17
18 -- data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where 18 -- data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
19 -- case1 : A → A ∨ B 19 -- case1 : A → A ∨ B
20 -- case2 : B → A ∨ B 20 -- case2 : B → A ∨ B
21 21
22 data ZFSet {n : Level} : Set (suc n) where 22 data ZFSet {n : Level} : Set (suc (suc n)) where
23 elem : { A : Set n } ( a : A ) → ZFSet 23 elem : { A : Set n } ( a : A ) → ZFSet
24 ∅ : ZFSet {n} 24 ∅ : ZFSet {n}
25 pair : {A B : Set n} (a : A ) (b : B ) → ZFSet 25 pair : {A B : Set n} (a : A ) (b : B ) → ZFSet
26 union : (A : ZFSet {n}) → ZFSet 26 union : (A : Set (suc n) ) → ZFSet
27 repl : { A B : Set n} → ( ψ : A → B ) → ZFSet 27 -- repl : ( ψ : ZFSet {n} → Set zero ) → ZFSet
28 infinite : ZFSet 28 infinite : ZFSet
29 power : (A : ZFSet {n}) → ZFSet 29 power : (A : ZFSet {n}) → ZFSet
30 30
31 infix 60 _∋_ _∈_ 31 infix 60 _∋_ _∈_
32 32
34 34
35 data _∈_ {n : Level} : {A : Set n} ( a : A ) ( Z : ZFSet {n} ) → Set (suc n) where 35 data _∈_ {n : Level} : {A : Set n} ( a : A ) ( Z : ZFSet {n} ) → Set (suc n) where
36 ∈-elm : {A : Set n } {a : A} → a ∈ (elem a) 36 ∈-elm : {A : Set n } {a : A} → a ∈ (elem a)
37 ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A} → a ∈ (pair a b) 37 ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A} → a ∈ (pair a b)
38 ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B} → b ∈ (pair a b) 38 ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B} → b ∈ (pair a b)
39 -- ∈-union : {Z : ZFSet {n}} {A : Set n} → { b : ZFSet {n} } → {!!} → a ∈ (union Z) 39 -- ∈-union : {Z : Set (suc n)} {A : Z } → {a : {!!} } → a ∈ (union Z)
40 ∈-repl : {A : Set n } { B : Set n} → { ψ : B → A } → { b : B } → ψ b ∈ (repl ψ) 40 -- ∈-repl : {A : Set n } { B : Set n} → { ψ : B → A } → { b : B } → ψ b ∈ {!!} -- (repl {!!})
41 -- ∈-infinite-1 : ∅ ∈ infinite 41 -- ∈-infinite-1 : ∅ ∈ infinite
42 -- ∈-infinite : {A : Set n} {a : A} → _∈_ infinite {A} a 42 -- ∈-infinite : {A : Set n} {a : A} → _∈_ infinite {A} a
43 ∈-power : {A : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈ (power Z) 43 ∈-power : {A B : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈ (power Z)
44 44
45 -- _∈_ : {n : Level} { A : ZFSet {n} } → {B : Set n} → (a : B ) → Set n → Bool 45 -- _∈_ : {n : Level} { A : ZFSet {n} } → {B : Set n} → (a : B ) → Set n → Bool
46 -- _∈_ {_} {A} a _ = A ∋ a 46 -- _∈_ {_} {A} a _ = A ∋ a
47 47
48 infix 40 _⇔_ 48 infix 40 _⇔_