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

comparison src/LEMC.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents d1c9f5ae5d0a
children e086a266c6b7
comparison
equal deleted inserted replaced
1095:08b6aa6870d9 1096:55ab5de1ae02
30 30
31 open import zfc 31 open import zfc
32 32
33 open HOD 33 open HOD
34 34
35 open _⊆_
36
37 decp : ( p : Set n ) → Dec p -- assuming axiom of choice 35 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
38 decp p with p∨¬p p 36 decp p with p∨¬p p
39 decp p | case1 x = yes x 37 decp p | case1 x = yes x
40 decp p | case2 x = no x 38 decp p | case2 x = no x
41 39
48 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice 46 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
49 ... | yes p = p 47 ... | yes p = p
50 ... | no ¬p = ⊥-elim ( notnot ¬p ) 48 ... | no ¬p = ⊥-elim ( notnot ¬p )
51 49
52 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 50 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
53 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where 51 power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where
54 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) 52 t1 : {x : HOD } → t ∋ x → A ∋ x
55 t1 = power→ A t PA∋t 53 t1 = power→ A t PA∋t
56 54
57 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice 55 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
58 --- 56 ---
59 record choiced ( X : Ordinal ) : Set n where 57 record choiced ( X : Ordinal ) : Set n where