{-# 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               ∎ 
      } 
    }