misc: move contradiction example to exercises

1 files changed, 44 insertions, 0 deletions

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})