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

open import Categories.Category

module Categories.Object.Subobject {o β„“ e} (π’ž : Category o β„“ e) where

open import Level
open import Data.Product
open import Data.Unit

open import Relation.Binary using (Poset)

open import Categories.Functor
open import Categories.Category.Slice
open import Categories.Category.SubCategory
open import Categories.Category.Construction.Thin
import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.Notation

private
  module π’ž = Category π’ž

-- The Full Subcategory of the over category π’ž/c on monomorphisms
slice-mono : π’ž.Obj β†’ Category _ _ _
slice-mono c = FullSubCategory (Slice π’ž c) {I = Ξ£[ Ξ± ∈ π’ž.Obj ](Ξ± ↣ c)} Ξ» (_ , i) β†’ sliceobj (mor i)
  where open Mor π’ž
        open _↣_

-- Poset of subobjects for some c ∈ π’ž
Subobjects : π’ž.Obj β†’ Poset _ _ _
Subobjects c = record
  { Carrier = π’žαΆœ.Obj
  ; _β‰ˆ_ = π’žαΆœ [_β‰…_]
  ; _≀_ = π’žαΆœ [_,_]
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Mor.β‰…-isEquivalence π’žαΆœ
      ; reflexive = Ξ» iso β†’ Mor._β‰…_.from iso
      ; trans = Ξ» {(Ξ± , f) (Ξ² , g) (Ξ³ , h)} i j β†’ slicearr (chase f g h i j)
      }
    ; antisym = Ξ» {(Ξ± , f) (Ξ² , g)} h i β†’ record
      { from = h
      ; to = i
      ; iso = record
        { isoΛ‘ = mono f _ _ (chase f g f h i β—‹ ⟺ π’ž.identityΚ³)
        ; isoΚ³ = mono g _ _ (chase g f g i h β—‹ ⟺ π’ž.identityΚ³)
        }
      }
    }
  }
  where
    π’žαΆœ : Category _ _ _
    π’žαΆœ = slice-mono c

    module π’žαΆœ = Category π’žαΆœ

    open Mor π’ž using (_↣_)
    open MR π’ž
    open π’ž.HomReasoning
    open _↣_

    chase : βˆ€ {Ξ± Ξ² Ξ³ : π’ž.Obj} (f : π’ž [ Ξ± ↣ c ]) (g : π’ž [ Ξ² ↣ c ]) (h : π’ž [ Ξ³ ↣ c ])
            β†’ (i : π’žαΆœ [ (Ξ± , f) , (Ξ² , g) ]) β†’ (j : π’žαΆœ [ (Ξ² , g) , (Ξ³ , h) ])
            β†’ π’ž [ π’ž [ mor h ∘ π’ž [ Sliceβ‡’.h j ∘ Sliceβ‡’.h i ] ] β‰ˆ mor f ]
    chase f g h i j = begin
      π’ž [ mor h ∘ π’ž [ Sliceβ‡’.h j ∘ Sliceβ‡’.h i ] ] β‰ˆβŸ¨ pullΛ‘ (Sliceβ‡’.β–³ j)  ⟩
      π’ž [ mor g ∘ Sliceβ‡’.h i ]                    β‰ˆβŸ¨ Sliceβ‡’.β–³ i ⟩
      mor f ∎