Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ODC.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 |
---|---|
67 decp : ( p : Set n ) → Dec p -- assuming axiom of choice | 67 decp : ( p : Set n ) → Dec p -- assuming axiom of choice |
68 decp p with p∨¬p p | 68 decp p with p∨¬p p |
69 decp p | case1 x = yes x | 69 decp p | case1 x = yes x |
70 decp p | case2 x = no x | 70 decp p | case2 x = no x |
71 | 71 |
72 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) | |
73 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM | |
74 ∋-p A x | case1 t = yes t | |
75 ∋-p A x | case2 t = no (λ x → t x) | |
76 | |
72 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic | 77 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic |
73 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice | 78 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice |
74 ... | yes p = p | 79 ... | yes p = p |
75 ... | no ¬p = ⊥-elim ( notnot ¬p ) | 80 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
76 | 81 |