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

module Categories.Adjoint.Instance.PosetCore where

-- The adjunction between the "forgetful" functor from Posets to
-- Setoids and the core functor for posets.

open import Level using (_⊔_)
import Function
open import Function.Bundles using (Func)
open import Relation.Binary using (Setoid; Poset)
open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
import Relation.Binary.Morphism.Construct.Composition as Comp

open import Categories.Adjoint using (_⊣_)
import Categories.Adjoint.Instance.0-Truncation as Setd
import Categories.Adjoint.Instance.01-Truncation as Pos
open import Categories.Category.Core using (Category)
open import Categories.Category.Construction.Thin using (Thin; module EqIsIso)
open import Categories.Category.Instance.Posets using (Posets)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor.Instance.Core using () renaming (Core to CatCore)
import Categories.Functor.Instance.Core as Cat
open import Categories.Functor using (Functor; _∘F_; id)
import Categories.Morphism as Morphism
open import Categories.Morphism.IsoEquiv using (⌞_⌟)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (_≃_; niHelper)

open PosetHomomorphism using (⟦_⟧; cong)

-- The "forgetful" functor from Setoids to Posets (forgetting symmetry).

open Func

Forgetful : ∀ {c ℓ} → Functor (Setoids c ℓ) (Posets c ℓ ℓ)
Forgetful = record
  { F₀           = Forgetful₀
  ; F₁           = λ f → mkPosetHomo _ _ (to f) (cong f)
  ; identity     = λ {S}       → refl S
  ; homomorphism = λ {_ _ S}   → refl S
  ; F-resp-≈     = λ {S _} f≗g → f≗g
  }
  where
    Forgetful₀ : ∀ {c ℓ} → Setoid c ℓ → Poset c ℓ ℓ
    Forgetful₀ S = record
      { _≈_               = _≈_
      ; _≤_               = _≈_
      ; isPartialOrder    = record
        { isPreorder      = record
          { isEquivalence = isEquivalence
          ; reflexive     = Function.id
          ; trans         = trans
          }
        ; antisym         = Function.const
        }
      }
      where open Setoid S

    open Setoid

-- The "core" functor from Posets to Setoids.
--
-- This functor simply forgets the _≤_ relation, mapping a Poset to
-- the Setoid over which it is defined.  This Setoid is the "core" of
-- the Poset in the sense that the "equality" _≈_ associated with the
-- Poset is really an equivalence, and antisymmetry ensures that this
-- equivalence is equivalent to the symmetric core of _≤_.

Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ₁)
Core = record
  { F₀           = λ A → record { isEquivalence = isEquivalence A }
  ; F₁           = λ f → record { to = ⟦ f ⟧ ; cong = cong f }
  ; identity     = λ {A} → Eq.refl A
  ; homomorphism = λ {_ _ Z} → Eq.refl Z
  ; F-resp-≈     = λ f≗g → f≗g
  }
  where open Poset

-- Core is right-adjoint to the forgetful functor

CoreAdj : ∀ {o ℓ} → Forgetful ⊣ Core {o} {ℓ} {ℓ}
CoreAdj = record
  { unit   = ntHelper record { η = unit   ; commute = λ {_} {Y} _ → Setoid.refl Y}
  ; counit = ntHelper record { η = counit ; commute = λ {_ B} _ → Eq.refl B }
  ; zig    = λ {S} → Setoid.refl S
  ; zag    = λ {B} → Eq.refl B
  }
  where
    open Poset
    open Functor Core      using () renaming (F₀ to Core₀; F₁ to Core₁)
    open Functor Forgetful using () renaming (F₀ to U₀   ; F₁ to U₁)

    unit : ∀ S → Func S (Core₀ (U₀ S))
    unit S = record { to = Function.id ; cong = Function.id }

    counit : ∀ A → PosetHomomorphism (U₀ (Core₀ A)) A
    counit A = mkPosetHomo (U₀ (Core₀ A)) A Function.id (reflexive A)

-- The core functor commutes with inclusion, i.e. the core of a thin
-- category is the 0-Groupoid generated by the associated equivalence.
--
-- Note that the core functor does not commute with truncation,
-- because the latter forgets too much (there are many more isos in
-- the (0,1)-truncated category).

Core-commutes : ∀ {c ℓ} e → Setd.Inclusion e ∘F Core ≃
                Cat.Core ∘F Pos.Inclusion {c} {ℓ ⊔ e} {ℓ} e
Core-commutes e = niHelper record
  { η   = λ A → record { F₀ = Function.id ; F₁ = EqIsIso.≈⇒≅ e A }
  ; η⁻¹ = λ A → record { F₀ = Function.id ; F₁ = EqIsIso.≅⇒≈ e A }
  ; commute = λ {A B} f →
    let open Morphism (Thin e B)
    in niHelper record { η   = λ _ → ≅.refl ; η⁻¹ = λ _ → ≅.refl }
  ; iso = λ A →
    let open Poset A
        open Morphism (Thin e A)
    in record
    { isoˡ = niHelper record { η = λ _ → Eq.refl ; η⁻¹ = λ _ → Eq.refl }
    ; isoʳ = niHelper record { η = λ _ → ≅.refl  ; η⁻¹ = λ _ → ≅.refl  }
    }
  }