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

diff ODC.agda @ 370:1425104bb5d8

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 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