From f6b13d677ae776182706ef0e46d9ccba5c2017f0 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick+github@patrickstevens.co.uk>
Date: Sun, 23 Feb 2020 12:16:19 +0000
Subject: [PATCH] Fix up the classical five to avoid duplicated work (#101)

---
 ClassicalLogic/ClassicalFive.agda | 28 ++++++++--------------------
 1 file changed, 8 insertions(+), 20 deletions(-)

diff --git a/ClassicalLogic/ClassicalFive.agda b/ClassicalLogic/ClassicalFive.agda
index 8f22c62..b685a66 100644
--- a/ClassicalLogic/ClassicalFive.agda
+++ b/ClassicalLogic/ClassicalFive.agda
@@ -9,6 +9,7 @@ em = {A : Set} → (A || (A → False))
 dne = {A : Set} → ((A → False) → False) → A
 peirce = {A B : Set} → ((A → B) → A) → A
 iad = {A B : Set} → (A → B) → ((A → False) || B)
+dem = {A B : Set} → (((A → False) && (B → False)) → False) → A || B
 
 emToDne : em → dne
 emToDne em {A} pr with em {A}
@@ -16,30 +17,17 @@ emToDne em {A} pr | inl x = x
 emToDne em {A} pr | inr x = exFalso (pr x)
 
 dneToPeirce : dne → peirce
-dneToPeirce dne {A} {B} aba = dne (λ z → z (aba (λ z₁ → dne (λ _ → z z₁))))
+dneToPeirce dne {A} {B} aba = dne (λ z → z (aba (λ a → dne (λ _ → z a))))
 
 peirceToIad : peirce → iad
 peirceToIad peirce {A} {B} aToB = peirce (λ z → inl (λ x → z (inr (aToB x))))
 
-iadToEm : iad → em
-iadToEm iad {A} with (iad {A} {A} (λ i → i))
-iadToEm iad {A} | inl x = inr x
-iadToEm iad {A} | inr x = inl x
-
-dem = {A B : Set} → (((A → False) && (B → False)) → False) → A || B
+iadToDem : iad → dem
+iadToDem iad {A} {B} x with iad {A} {A} (λ i → i)
+iadToDem iad {A} {B} x | inl notA with iad {B} {B} (λ i → i)
+iadToDem iad {A} {B} x | inl notA | inl notB = exFalso (x (notA ,, notB))
+iadToDem iad {A} {B} x | inl notA | inr b = inr b
+iadToDem iad {A} {B} x | inr a = inl a
 
 demToEm : dem → em
 demToEm dem {A} = dem (λ z → _&&_.snd z (_&&_.fst z))
-
-emToDem : em → dem
-emToDem em {A} {B} pr with em {A}
-emToDem em {A} {B} pr | inl x = inl x
-emToDem em {A} {B} pr | inr x with em {B}
-emToDem em {A} {B} pr | inr x | inl x₁ = inr x₁
-emToDem em {A} {B} pr | inr x | inr y = exFalso (pr (x ,, y))
-
-isContr : {a : _} (A : Set a) → Set a
-isContr T = (x y : T) → x ≡ y
-
-pr : {a : _} {A : Set a} → {x : A} → isContr (Sg A (λ y → x ≡ y))
-pr {A = A} {.a} (a , refl) (.a , refl) = refl