1 files changed, 42 insertions, 0 deletions
diff --git a/src/CatTheory/Exercise1/Contradiction/SetoidsTwoEqThree.agda b/src/CatTheory/Exercise1/Contradiction/SetoidsTwoEqThree.agda
new file mode 100644
index 0000000..0c1431c
--- /dev/null
+++ b/src/CatTheory/Exercise1/Contradiction/SetoidsTwoEqThree.agda
@@ -0,0 +1,42 @@
+{-# OPTIONS --safe --without-K #-}
+
+module CatTheory.Exercise1.Contradiction.SetoidsTwoEqThree where
+
+open import Categories.Category using (Category)
+import Categories.Morphism as Morphism
+import Categories.Morphism.Properties as Morphismₚ
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Data.Fin using (Fin; zero; suc)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Function using (_$_)
+open import Function.Equality using (_⟨$⟩_)
+open import Level using (0ℓ)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
+
+open Category (Setoids 0ℓ 0ℓ)
+open Morphism (Setoids 0ℓ 0ℓ)
+open Morphismₚ (Setoids 0ℓ 0ℓ)
+
+2≇3 : ¬ setoid (Fin 2) ≅ setoid (Fin 3)
+2≇3 2≅3 = contradiction helper [ (λ ()) , [ (λ ()) , (λ ()) ]′ ]′
+  where
+  open _≅_ 2≅3
+  open ≡-Reasoning
+
+  to-injective : ∀ {x y} → to ⟨$⟩ x ≡ to ⟨$⟩ y → x ≡ y
+  to-injective {x} {y} eq = begin
+    x                   ≡˘⟨ isoʳ refl ⟩
+    from ⟨$⟩ (to ⟨$⟩ x) ≡⟨  cong (from ⟨$⟩_) eq ⟩
+    from ⟨$⟩ (to ⟨$⟩ y) ≡⟨  isoʳ refl ⟩
+    y                   ∎
+
+  helper : (zero {2} ≡ suc zero) ⊎ (zero {2} ≡ suc (suc zero)) ⊎ (suc {2} zero ≡ suc (suc zero))
+  helper with to ⟨$⟩ zero in eq₀ | to ⟨$⟩ suc zero in eq₁ | to ⟨$⟩ suc (suc zero) in eq₂
+  ... | zero     | zero     | _        = inj₁ $ to-injective $ trans eq₀ (sym eq₁)
+  ... | zero     | suc zero | zero     = inj₂ $ inj₁ $ to-injective $ trans eq₀ (sym eq₂)
+  ... | zero     | suc zero | suc zero = inj₂ $ inj₂ $ to-injective $ trans eq₁ (sym eq₂)
+  ... | suc zero | zero     | zero     = inj₂ $ inj₂ $ to-injective $ trans eq₁ (sym eq₂)
+  ... | suc zero | zero     | suc zero = inj₂ $ inj₁ $ to-injective $ trans eq₀ (sym eq₂)
+  ... | suc zero | suc zero | _        = inj₁ $ to-injective $ trans eq₀ (sym eq₁)