diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 15:33:41 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2022-01-05 15:33:41 +0000 |
| commit | e29c60d82f51f61c0649fef81536b4e5029a914d (patch) | |
| tree | c7b2824e7a752a64a544b83e75881cd57df9c735 | |
| parent | 34b3cf760e2e56542092c0da587cd43c4fa90939 (diff) | |
I: 1: a: show 2 ≇ 3 in Setoids
| -rw-r--r-- | src/CatTheory/Exercise1/Contradiction/SetoidsTwoEqThree.agda | 42 |
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₁) |