diff zf.agda @ 188:1f2c8b094908

axiom of choice → p ∨ ¬ p
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2019 13:11:21 +0900
parents 914cc522c53a
children 64ef1db53c49
line wrap: on
line diff
--- a/zf.agda	Tue Jul 23 11:08:24 2019 +0900
+++ b/zf.agda	Thu Jul 25 13:11:21 2019 +0900
@@ -21,6 +21,8 @@
 
 open import Relation.Nullary
 open import Relation.Binary
+open import Data.Empty
+
 
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a ) 
@@ -28,6 +30,16 @@
 double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
 double-neg A notnot = notnot A
 
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+-- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
+-- mid-ex-neg {n} {A} = {!!}
+
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_