{-# 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₁)