blob: 0c1431c2f0975e4a46424aca7e60aeeb178406d4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
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₁)
|
