Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 370:1425104bb5d8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 12:26:17 +0900 |
parents | 17adeeee0c2a |
children | 6c72bee25653 |
comparison
equal
deleted
inserted
replaced
369:17adeeee0c2a | 370:1425104bb5d8 |
---|---|
38 OD→ZFC = record { | 38 OD→ZFC = record { |
39 ZFSet = HOD | 39 ZFSet = HOD |
40 ; _∋_ = _∋_ | 40 ; _∋_ = _∋_ |
41 ; _≈_ = _=h=_ | 41 ; _≈_ = _=h=_ |
42 ; ∅ = od∅ | 42 ; ∅ = od∅ |
43 ; Select = ? | 43 ; Select = {!!} |
44 ; isZFC = isZFC | 44 ; isZFC = isZFC |
45 } where | 45 } where |
46 -- infixr 200 _∈_ | 46 -- infixr 200 _∈_ |
47 -- infixr 230 _∩_ _∪_ | 47 -- infixr 230 _∩_ _∪_ |
48 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ ? | 48 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ {!!} |
49 isZFC = record { | 49 isZFC = record { |
50 choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); | 50 choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); |
51 choice = λ A {X} A∋X not → is-in (choice-func X not) | 51 choice = λ A {X} A∋X not → is-in (choice-func X not) |
52 } where | 52 } where |
53 -- | 53 -- |