From 89ba967e8f458abecde49006a7c1761af765c520 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 6 Jan 2022 18:17:12 +0000
Subject: misc: move contradiction example to exercises

---
 .../Instance/Properties/Setoids/Contradiction.agda | 44 ----------------------
 .../Contradiction/SetoidsRetractsUnique.agda       | 44 ++++++++++++++++++++++
 2 files changed, 44 insertions(+), 44 deletions(-)
 delete mode 100644 src/CatTheory/Category/Instance/Properties/Setoids/Contradiction.agda
 create mode 100644 src/CatTheory/Exercise1/Contradiction/SetoidsRetractsUnique.agda

(limited to 'src')

diff --git a/src/CatTheory/Category/Instance/Properties/Setoids/Contradiction.agda b/src/CatTheory/Category/Instance/Properties/Setoids/Contradiction.agda
deleted file mode 100644
index 1a553d3..0000000
--- a/src/CatTheory/Category/Instance/Properties/Setoids/Contradiction.agda
+++ /dev/null
@@ -1,44 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module CatTheory.Category.Instance.Properties.Setoids.Contradiction where
-
-open import Categories.Category using (Category)
-open import Categories.Category.Instance.Setoids
-import Categories.Morphism as M
-open import Data.Bool using (Bool; true; false)
-open import Data.Nat using (ℕ; suc)
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Structures using (IsInjection)
-open import Level using (0ℓ)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
-
-module Monomorphisms where
-  open Category (Setoids 0ℓ 0ℓ)
-  open M (Setoids 0ℓ 0ℓ)
-
-  f : setoid Bool ⇒ setoid ℕ
-  f = record { _⟨$⟩_ = λ { true → 0 ; false → 1 } ; cong = cong _ }
-
-  g₁ : setoid ℕ ⇒ setoid Bool
-  g₁ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → true } ; cong = cong _ }
-
-  g₂ : setoid ℕ ⇒ setoid Bool
-  g₂ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → false } ; cong = cong _ }
-
-  g₁∘f≈id : g₁ RetractOf f
-  g₁∘f≈id {false} refl = refl
-  g₁∘f≈id {true}  refl = refl
-
-  g₂∘f≈id : g₂ RetractOf f
-  g₂∘f≈id {false} refl = refl
-  g₂∘f≈id {true}  refl = refl
-
-  g₁≉g₂ : ¬ g₁ ≈ g₂
-  g₁≉g₂ g₁≈g₂ = contradiction true≡false (λ ())
-    where
-    open ≡-Reasoning
-
-    true≡false : true ≡ false
-    true≡false = g₁≈g₂ (refl {x = 3})
diff --git a/src/CatTheory/Exercise1/Contradiction/SetoidsRetractsUnique.agda b/src/CatTheory/Exercise1/Contradiction/SetoidsRetractsUnique.agda
new file mode 100644
index 0000000..12aa82b
--- /dev/null
+++ b/src/CatTheory/Exercise1/Contradiction/SetoidsRetractsUnique.agda
@@ -0,0 +1,44 @@
+{-# OPTIONS --without-K --safe #-}
+
+module CatTheory.Exercise1.Contradiction.SetoidsRetractsUnique where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Setoids
+import Categories.Morphism as M
+open import Data.Bool using (Bool; true; false)
+open import Data.Nat using (ℕ; suc)
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Structures using (IsInjection)
+open import Level using (0ℓ)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
+
+module Monomorphisms where
+  open Category (Setoids 0ℓ 0ℓ)
+  open M (Setoids 0ℓ 0ℓ)
+
+  f : setoid Bool ⇒ setoid ℕ
+  f = record { _⟨$⟩_ = λ { true → 0 ; false → 1 } ; cong = cong _ }
+
+  g₁ : setoid ℕ ⇒ setoid Bool
+  g₁ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → true } ; cong = cong _ }
+
+  g₂ : setoid ℕ ⇒ setoid Bool
+  g₂ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → false } ; cong = cong _ }
+
+  g₁∘f≈id : g₁ RetractOf f
+  g₁∘f≈id {false} refl = refl
+  g₁∘f≈id {true}  refl = refl
+
+  g₂∘f≈id : g₂ RetractOf f
+  g₂∘f≈id {false} refl = refl
+  g₂∘f≈id {true}  refl = refl
+
+  g₁≉g₂ : ¬ g₁ ≈ g₂
+  g₁≉g₂ g₁≈g₂ = contradiction true≡false (λ ())
+    where
+    open ≡-Reasoning
+
+    true≡false : true ≡ false
+    true≡false = g₁≈g₂ (refl {x = 3})
-- 
cgit v1.2.3