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

open import Categories.Category.Core using (Category)
open import Categories.Category.Restriction using (Restriction)
open import Relation.Binary.Bundles using (Poset)
open import Relation.Binary.Structures using (IsPartialOrder)

import Categories.Morphism.Reasoning as MR

-- Every restriction category induces a partial order (the restriction order) on hom-sets

module Categories.Category.Restriction.Properties.Poset {o β„“ e} {π’ž : Category o β„“ e} (R : Restriction π’ž) where
  open Category π’ž
  open Restriction R
  open Equiv
  open HomReasoning
  open MR π’ž using (pullΚ³; pullΛ‘)

  poset : (A B : Obj) β†’ Poset β„“ e e
  poset A B = record
    { Carrier = A β‡’ B
    ; _β‰ˆ_ = _β‰ˆ_
    ; _≀_ = Ξ» f g β†’ f β‰ˆ g ∘ f ↓
    ; isPartialOrder = record
      { isPreorder = record
        { isEquivalence = equiv
        ; reflexive = Ξ» {x} {y} xβ‰ˆy β†’ begin
          x       β‰ˆΛ˜βŸ¨ pidΚ³ ⟩
          x ∘ x ↓ β‰ˆβŸ¨ xβ‰ˆy ⟩∘⟨refl ⟩
          y ∘ x ↓ ∎
        ; trans = Ξ» {i} {j} {k} iβ‰ˆj∘i↓ jβ‰ˆk∘j↓ β†’ begin
          i               β‰ˆβŸ¨ iβ‰ˆj∘i↓ ⟩
          j ∘ i ↓         β‰ˆβŸ¨ jβ‰ˆk∘j↓ ⟩∘⟨refl ⟩
          (k ∘ j ↓) ∘ i ↓ β‰ˆβŸ¨ pullΚ³ (sym ↓-denestΚ³) ⟩
          k ∘ (j ∘ i ↓) ↓ β‰ˆβŸ¨ refl⟩∘⟨ ↓-cong (sym iβ‰ˆj∘i↓) ⟩
          k ∘ i ↓         ∎
        }
      ; antisym = Ξ» {i} {j} iβ‰ˆj∘i↓ jβ‰ˆi∘j↓ β†’ begin
        i               β‰ˆβŸ¨ iβ‰ˆj∘i↓ ⟩
        j ∘ i ↓         β‰ˆβŸ¨ jβ‰ˆi∘j↓ ⟩∘⟨refl ⟩
        (i ∘ j ↓) ∘ i ↓ β‰ˆβŸ¨ pullΚ³ ↓-comm ⟩
        i ∘ i ↓ ∘ j ↓   β‰ˆβŸ¨ pullΛ‘ pidΚ³ ⟩
        i ∘ j ↓         β‰ˆΛ˜βŸ¨ jβ‰ˆi∘j↓ ⟩
        j               ∎
      }
    }