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

comparison ODC.agda @ 376:6c72bee25653

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Jul 2020 16:28:12 +0900
parents 1425104bb5d8
children 8b0715e28b33
comparison
equal deleted inserted replaced
375:8cade5f660bd 376:6c72bee25653
91 HOD→ZFC = record { 91 HOD→ZFC = record {
92 ZFSet = HOD 92 ZFSet = HOD
93 ; _∋_ = _∋_ 93 ; _∋_ = _∋_
94 ; _≈_ = _=h=_ 94 ; _≈_ = _=h=_
95 ; ∅ = od∅ 95 ; ∅ = od∅
96 ; Select = {!!} 96 ; Select = Select
97 ; isZFC = isZFC 97 ; isZFC = isZFC
98 } where 98 } where
99 -- infixr 200 _∈_ 99 -- infixr 200 _∈_
100 -- infixr 230 _∩_ _∪_ 100 -- infixr 230 _∩_ _∪_
101 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ {!!} 101 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
102 isZFC = record { 102 isZFC = record {
103 choice-func = choice-func ; 103 choice-func = choice-func ;
104 choice = choice 104 choice = choice
105 } where 105 } where
106 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) 106 -- Axiom of choice ( is equivalent to the existence of minimal in our case )