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

open import Relation.Binary using (Poset)

-- A thin (or posetal) category is a category with at most one
-- morphism between any pair of objects.
--
-- As explained on nLab:
--
--   "Up to isomorphism, a thin category is the same thing as a
--   proset. Up to equivalence, a thin category is the same thing as a
--   poset. (...) (It is really a question of whether you're working
--   with strict categories, which are classified up to isomorphism,
--   or categories as such, which are classified up to equivalence.)"
--
--                  -- https://ncatlab.org/nlab/show/thin+category
--
-- Since
--
--  1. posets in the standard library are defined up to an underlying
--     equivalence/setoid, but
--
--  2. categories in this library do not have a notion of equality on
--     objects (i.e. objects are considered up to isomorphism),
--
-- it makes sense to work with the weaker notion of thin categories
-- here, i.e. those generated by posets rather than prosets.  This
-- means that the core of a thin category (the groupoid consisting of
-- all its isomorphism) is just the setoid underlying the
-- corresponding poset.
--
-- (See Categories.Adjoint.Instance.PosetCore for more details.)

module Categories.Category.Construction.Thin {o ℓ₁ ℓ₂} e (P : Poset o ℓ₁ ℓ₂) where

open import Level
open import Data.Unit using (⊤)
open import Function using (flip)

open import Categories.Category
import Categories.Morphism as Morphism

open Poset P

Thin : Category o ℓ₂ e
Thin = record
  { Obj       = Carrier
  ; _⇒_       = _≤_
  ; _≈_       = λ _ _ → Lift e ⊤
  ; id        = refl
  ; _∘_       = flip trans
  ; assoc     = _
  ; identityˡ = _
  ; identityʳ = _
  ; equiv     = _
  ; ∘-resp-≈  = _
  }

module EqIsIso where

  open Category Thin hiding (_≈_)
  open Morphism Thin using (_≅_)
  open _≅_

  -- Equivalent elements of |P| are isomorphic objects of |Thin P|.

  ≈⇒≅ : ∀ {x y : Obj} → x ≈ y → x ≅ y
  ≈⇒≅ x≈y = record
    { from = reflexive x≈y
    ; to   = reflexive (Eq.sym x≈y)
    }

  ≅⇒≈ : ∀ {x y : Obj} → x ≅ y → x ≈ y
  ≅⇒≈ x≅y = antisym (from x≅y) (to x≅y)