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

module CatTheory.Category.Instance.Properties.Setoids where

open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids
import Categories.Morphism as M
open import Data.Bool using (if_then_else_)
open import Data.Empty using (⊥-elim)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Product using (∃; _,_)
open import Data.Unit.Polymorphic using (⊤)
open import Function using () renaming (id to idf)
open import Function.Equality using (_⟨$⟩_; cong)
open import Function.Structures using (IsInjection; IsSurjection)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
import Relation.Binary.Reasoning.Setoid as Reasoning
open import Relation.Nullary using (does; yes; no)
open import Relation.Nullary.Construct.Add.Point
open import Relation.Nullary.Decidable.Core using (True; toWitness)
open import Relation.Unary using (Decidable)

open Setoid renaming (_≈_ to ₍_₎_≈_)

module Monomorphisms {o l} where
  open Category (Setoids o l)
  open M (Setoids o l)

  Mono⇒IsInjection : ∀ {A B : Setoid o l} {f : A ⇒ B} → Mono f → IsInjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_)
  Mono⇒IsInjection {A} {B} {f} mono = record
    { isCongruent = record
      { cong = cong f
      ; isEquivalence₁ = isEquivalence A
      ; isEquivalence₂ = isEquivalence B
      }
    ; injective   = λ {x} {y} fx≈fy → mono {C = ⊤-setoid} (point x) (point y) (λ _ → fx≈fy) _
    }
    where
    ⊤-setoid : Setoid o l
    ⊤-setoid = record
      { Carrier = ⊤
      ; _≈_ = λ _ _ → ⊤
      ; isEquivalence = _
      }

    point : Carrier A → ⊤-setoid ⇒ A
    point x = record { _⟨$⟩_ = λ _ → x ; cong = λ _ → refl A }

  IsInjection⇒Mono : ∀ {A B : Setoid o l} {f : A ⇒ B} → IsInjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_) → Mono f
  IsInjection⇒Mono {A} {B} {f} isInjection g₁ g₂ f∘g₁≈f∘g₂ x≈y = injective (f∘g₁≈f∘g₂ x≈y)
    where open IsInjection isInjection

module Epimorphisms {o l} where
  open Category (Setoids o l)
  open M (Setoids o l)

  IsSujection⇒Epi : ∀ {A B : Setoid o l} {f : A ⇒ B} → IsSurjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_) → Epi f
  IsSujection⇒Epi {A} {B} {f} isSurjection {C} g₁ g₂ g₁∘f≈g₂∘f {x} {y} x≈y with surjective x
    where open IsSurjection isSurjection
  ... | a , fa≈x = begin
    g₁ ⟨$⟩ x         ≈˘⟨ cong g₁ fa≈x ⟩
    g₁ ⟨$⟩ (f ⟨$⟩ a) ≈⟨  g₁∘f≈g₂∘f (refl A) ⟩
    g₂ ⟨$⟩ (f ⟨$⟩ a) ≈⟨  cong g₂ fa≈x ⟩
    g₂ ⟨$⟩ x         ≈⟨  cong g₂ x≈y ⟩
    g₂ ⟨$⟩ y         ∎
    where open Reasoning C

  Epi⇒IsSurjection : ∀ {A B : Setoid o l} {f : A ⇒ B} →
                     Decidable (λ y → ∃ λ x → ₍ B ₎ f ⟨$⟩ x ≈ y) →
                     Epi f →
                     IsSurjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_)
  Epi⇒IsSurjection {A} {B} {f} image? epi = record
    { isCongruent = record
      { cong = cong f
      ; isEquivalence₁ = isEquivalence A
      ; isEquivalence₂ = isEquivalence B
      }
    ; surjective = λ y → toWitness (imageTrue y)
    }
    where
    _≈∙_ : Pointed (Carrier B) → Pointed (Carrier B) → Set l
    [ x ] ≈∙ [ y ] = ₍ B ₎ x ≈ y
    [ x ] ≈∙ ∙     = ⊥
    ∙     ≈∙ [ y ] = ⊥
    ∙     ≈∙ ∙     = ⊤

    ≈∙-refl : Reflexive _≈∙_
    ≈∙-refl {[ x ]} = refl B
    ≈∙-refl {∙}     = _

    ≈∙-sym : Symmetric _≈∙_
    ≈∙-sym {[ x ]} {[ y ]} x≈y = sym B x≈y
    ≈∙-sym {∙}     {∙}     _   = _

    ≈∙-trans : Transitive _≈∙_
    ≈∙-trans {[ x ]} {[ y ]} {[ z ]} x≈y y≈z = trans B x≈y y≈z
    ≈∙-trans {∙}     {∙}     {∙}     _   _   = _

    -- Need these levels or we cannot use epi.
    -- Otherwise, use Relation.Binary.Contruct.Add.Point.Equality.
    C : Setoid o l
    C = record
      { _≈_ = _≈∙_
      ; isEquivalence = record
        { refl = λ {x} → ≈∙-refl {x}
        ; sym = λ {x} {y} → ≈∙-sym {x} {y}
        ; trans = λ {x} {y} {z} → ≈∙-trans {x} {y} {z}
        }
      }

    g₁ : B ⇒ C
    g₁ = record { _⟨$⟩_ = [_] ; cong = idf }

    g₂ : B ⇒ C
    g₂ = record
      { _⟨$⟩_ = map
      ; cong = λ i≈j → map-cong i≈j
      }
      where
      map = λ y → if does (image? y) then [ y ] else ∙

      map-cong : ∀ {i j} → ₍ B ₎ i ≈ j → ₍ C ₎ map i ≈ map j
      map-cong {i} {j} i≈j with image? i | image? j
      ... | yes _          | yes _          = i≈j
      ... | yes (a , fa≈i) | no ¬fx≈j       = ⊥-elim (¬fx≈j (a , trans B fa≈i i≈j))
      ... | no ¬fx≈i       | yes (b , fb≈j) = ⊥-elim (¬fx≈i (b , trans B fb≈j (sym B i≈j)))
      ... | no _           | no _           = _

    g₁∘f≈g₂∘f : g₁ ∘ f ≈ g₂ ∘ f
    g₁∘f≈g₂∘f {x} {y} x≈y with image? (f ⟨$⟩ y)
    ... | yes _      = cong f x≈y
    ... | no ¬∃fz≈fy = ⊥-elim (¬∃fz≈fy (y , refl B))

    g₁≈g₂ : g₁ ≈ g₂
    g₁≈g₂ = epi g₁ g₂ g₁∘f≈g₂∘f

    imageTrue : ∀ y → True (image? y)
    imageTrue y with image? y | g₁≈g₂ {y} (refl B)
    ... | yes _ | _ = _