moving LogicAns to NegationAns

src/Logic.lagda

@@ -142,10 +142,10 @@ and similarly for `invʳ`, which does the same (up to renaming).
 ×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A)
 ×-comm =
   record
-    { to = λ { (x , y) → (y , x)}
-    ; fro = λ { (y , x) → (x , y)}
-    ; invˡ = λ { (x , y) → refl }
-    ; invʳ = λ { (y , x) → refl }
+    { to      = λ { (x , y) → (y , x)}
+    ; from    = λ { (y , x) → (x , y)}
+    ; from∘to = λ { (x , y) → refl }
+    ; to∘from = λ { (y , x) → refl }
     } 
 \end{code}
 
@@ -171,10 +171,10 @@ matching against a suitable pattern to enable simplificition.
 ×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C))
 ×-assoc =
   record
-    { to = λ { ((x , y) , z) → (x , (y , z)) }
-    ; fro = λ { (x , (y , z)) → ((x , y) , z) }
-    ; invˡ = λ { ((x , y) , z) → refl }
-    ; invʳ = λ { (x , (y , z)) → refl }
+    { to      = λ { ((x , y) , z) → (x , (y , z)) }
+    ; from    = λ { (x , (y , z)) → ((x , y) , z) }
+    ; from∘to = λ { ((x , y) , z) → refl }
+    ; to∘from = λ { (x , (y , z)) → refl }
     } 
 \end{code}
 
@@ -237,10 +237,10 @@ a suitable pattern to enable simplification.
 ⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A
 ⊤-identityˡ =
   record
-    { to   = λ { (tt , x) → x }
-    ; fro  = λ { x → (tt , x) }
-    ; invˡ = λ { (tt , x) → refl }
-    ; invʳ = λ { x → refl}
+    { to      = λ { (tt , x) → x }
+    ; from    = λ { x → (tt , x) }
+    ; from∘to = λ { (tt , x) → refl }
+    ; to∘from = λ { x → refl}
     }
 \end{code}
 
@@ -343,18 +343,18 @@ does the same (up to renaming).
 \begin{code}
 ⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A)
 ⊎-comm = record
-  { to   = λ { (inj₁ x) → (inj₂ x)
-             ; (inj₂ y) → (inj₁ y)
-             }
-  ; fro  = λ { (inj₁ y) → (inj₂ y)
-             ; (inj₂ x) → (inj₁ x)
-             }
-  ; invˡ = λ { (inj₁ x) → refl
-             ; (inj₂ y) → refl
-             }
-  ; invʳ = λ { (inj₁ y) → refl
-             ; (inj₂ x) → refl
-             }
+  { to      = λ { (inj₁ x) → (inj₂ x)
+              ; (inj₂ y) → (inj₁ y)
+              }
+  ; from    = λ { (inj₁ y) → (inj₂ y)
+              ; (inj₂ x) → (inj₁ x)
+              }
+  ; from∘to = λ { (inj₁ x) → refl
+                ; (inj₂ y) → refl
+                } 
+  ; to∘from = λ { (inj₁ y) → refl
+                ; (inj₂ x) → refl
+                }  
   }
 \end{code}
 Being *commutative* is different from being *commutative up to

src/LogicAns.lagda

@@ -1,52 +0,0 @@
----
-title     : "Logic Answers"
-layout    : page
-permalink : /LogicAns
----
-
-\begin{code}
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
-open import Isomorphism using (_≃_)
-open import Logic
-\end{code}
-
-
-*Equivalences for classical logic*
-
-\begin{code}
-ex1 : ¬¬-elim → excluded-middle
-ex1 h = h excluded-middle-irrefutable
-
-ex2 : excluded-middle → implication
-ex2 em f with em
-... | inj₁ a = inj₂ (f a)
-... | inj₂ ¬a = inj₁ ¬a
-
-ex3 : excluded-middle → peirce
-ex3 em k with em
-... | inj₁ a = a
-... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a))
-
-help′ : excluded-middle → ∀ {A B : Set} → ¬ (A × B) → ¬ A ⊎ ¬ B
-help′ em ¬a×b with em | em
-... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b))
-... | inj₁ a | inj₂ ¬b = inj₂ ¬b
-... | inj₂ ¬a | inj₁ b = inj₁ ¬a
-... | inj₂ ¬a | inj₂ ¬b = inj₁ ¬a
-
-⊤⊥-iso : (¬ ⊥) ≃ ⊤
-⊤⊥-iso =
-  record
-    { to   =  λ _ → tt
-    ; fro  =  λ _ ff → ff
-    ; invˡ =  λ _ → extensionality (λ ())
-    ; invʳ =  λ { tt → refl }
-    }
-\end{code}  
-
-*Existentials and Universals*
-
-\begin{code}
-∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)
-∃¬¬∀ (x , ¬bx) ∀bx = ¬bx (∀bx x)
-\end{code}

src/Negation.lagda

@@ -265,13 +265,14 @@ Philip Wadler, *International Conference on Functional Programming*, 2003.)
 
 ### Exercise
 
-Prove the following three formulas are equivalent to each other,
-and to the formulas `EM` and `⊎-Dual-+` given earlier.
+Prove the following four formulas are equivalent to each other,
+and to the formula `EM` given earlier.
 \begin{code}
 ¬¬-Elim Peirce Implication : Set₁
 ¬¬-Elim = ∀ {A : Set} → ¬ ¬ A → A
 Peirce = ∀ {A B : Set} → (((A → B) → A) → A)
 Implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
+×-Implies-⊎ = ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B)
 \end{code}
 
     

src/NegationAns.lagda

@@ -0,0 +1,67 @@
+---
+title     : "Logic Answers"
+layout    : page
+permalink : /LogicAns
+---
+
+\begin{code}
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Isomorphism using (_≃_)
+open import Negation using
+  (¬_; id; EM; em-irrefutable; ¬¬-Elim; Peirce; Implication; ×-Implies-⊎)
+\end{code}
+
+In what follows, we occasionally require [extensionality][extensionality].
+\begin{code}
+postulate
+  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
+\end{code}
+
+[extensionality]: Equality/index.html#extensionality
+
+
+
+*Equivalences for classical logic*
+
+\begin{code}
+ex1 : ¬¬-Elim → EM
+ex1 h = h em-irrefutable
+
+ex2 : EM → Implication
+ex2 em f with em
+... | inj₁ a = inj₂ (f a)
+... | inj₂ ¬a = inj₁ ¬a
+
+ex3 : EM → Peirce
+ex3 em k with em
+... | inj₁ a = a
+... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a))
+
+ex4 : EM → ×-Implies-⊎
+ex4 em ¬a×b with em | em
+... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b))
+... | inj₁ a | inj₂ ¬b = inj₂ ¬b
+... | inj₂ ¬a | _ = inj₁ ¬a
+
+⊤⊥-iso : (¬ ⊥) ≃ ⊤
+⊤⊥-iso =
+  record
+    { to      =  λ{ _ → tt }
+    ; from    =  λ{ _ → id }
+    ; from∘to =  λ{ _ → extensionality (λ ()) }
+    ; to∘from =  λ{ tt → refl }
+    }
+\end{code}  
+
+*Existentials and Universals*
+
+\begin{code}
+{-
+∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)
+∃¬¬∀ (x , ¬bx) ∀bx = ¬bx (∀bx x)
+-}
+\end{code}