Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/ODC.agda Sun Jul 19 10:02:43 2020 +0900 +++ b/ODC.agda Sun Jul 19 12:26:17 2020 +0900 @@ -69,6 +69,11 @@ decp p | case1 x = yes x decp p | case2 x = no x +∋-p : (A x : HOD ) → Dec ( A ∋ x ) +∋-p A x with p∨¬p ( A ∋ x ) -- LEM +∋-p A x | case1 t = yes t +∋-p A x | case2 t = no (λ x → t x) + double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic double-neg-eilm {A} notnot with decp A -- assuming axiom of choice ... | yes p = p