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

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