{-# OPTIONS --without-K --safe #-}

module CatTheory.Exercise1.Contradiction.SetoidsRetractsUnique 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})