misc: move contradiction example to exercises

1 files changed, 0 insertions, 44 deletions

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