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

-- Some properties of Restriction Categories

-- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
module Categories.Category.Restriction.Properties where

open import Data.Product using (Ξ£; _,_)
open import Level using (Level; _βŠ”_)

open import Categories.Category.Core using (Category)
open import Categories.Category.Restriction using (Restriction)
open import Categories.Category.SubCategory
open import Categories.Morphism using (Mono)
open import Categories.Morphism.Idempotent using (Idempotent)
open import Categories.Morphism.Properties using (Mono-id)
import Categories.Morphism.Reasoning as MR

module _ {o β„“ e : Level} {π’ž : Category o β„“ e} (R : Restriction π’ž) where
  open Category π’ž
  open Restriction R
  open HomReasoning
  open MR π’ž using (elimΛ‘; introΚ³)

  private
    variable
      A B C : Obj
      f : A β‡’ B
      g : B β‡’ C

  ↓f-idempotent : (A β‡’ B) β†’ Idempotent π’ž A
  ↓f-idempotent f = record { idem = f ↓ ; idempotent = ⟺ ↓-denestΚ³ β—‹ ↓-cong pidΚ³ }

  -- a special version of ↓ being a partial left identity
  ↓-pidΛ‘-gf : f ↓ ∘ (g ∘ f) ↓ β‰ˆ (g ∘ f) ↓
  ↓-pidΛ‘-gf {f = f} {g = g} = begin
    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-comm ⟩
    (g ∘ f) ↓ ∘ f ↓   β‰ˆΛ˜βŸ¨ ↓-denestΚ³ ⟩
    ((g ∘ f) ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-cong assoc ⟩
    (g ∘ (f ∘ f ↓)) ↓ β‰ˆβŸ¨ ↓-cong (∘-resp-β‰ˆΚ³ pidΚ³) ⟩
    (g ∘ f) ↓ ∎

  -- left denesting looks different in its conclusion
  ↓-denestΛ‘ : (g ↓ ∘ f) ↓ β‰ˆ (g ∘ f) ↓
  ↓-denestΛ‘ {g = g} {f = f} = begin
    (g ↓ ∘ f) ↓       β‰ˆβŸ¨ ↓-cong ↓-skew-comm ⟩
    (f ∘ (g ∘ f) ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
    (g ∘ f) ↓         ∎

  ↓-idempotent : f ↓ ↓ β‰ˆ f ↓
  ↓-idempotent {f = f} = begin
    f ↓ ↓        β‰ˆΛ˜βŸ¨ ↓-cong identityΚ³ ⟩
    (f ↓ ∘ id) ↓ β‰ˆβŸ¨ ↓-denestΛ‘ ⟩
    (f ∘ id) ↓   β‰ˆβŸ¨ ↓-cong identityΚ³ ⟩
    f ↓ ∎

  ↓↓denest : (g ↓ ∘ f ↓) ↓ β‰ˆ g ↓ ∘ f ↓
  ↓↓denest {g = g} {f = f} = begin
    (g ↓ ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
    g ↓ ↓ ∘ f ↓   β‰ˆβŸ¨ (↓-idempotent ⟩∘⟨refl) ⟩
    g ↓ ∘ f ↓ ∎

  Monoβ‡’fβ†“β‰ˆid : Mono π’ž f β†’ f ↓ β‰ˆ id
  Monoβ‡’fβ†“β‰ˆid {f = f} mono = mono (f ↓) id (pidΚ³ β—‹ ⟺ identityΚ³)

  -- if the domain of g is at least that of f, then the restriction coincides
  β†“βŠƒβ‡’β‰ˆ : f ∘ g ↓ β‰ˆ f β†’ f ↓ β‰ˆ f ↓ ∘ g ↓
  β†“βŠƒβ‡’β‰ˆ {f = f} {g = g} fgβ†“β‰ˆf = ⟺ (↓-cong fgβ†“β‰ˆf) β—‹ ↓-denestΚ³

  Monoβ‡’Total : Mono π’ž f β†’ total f
  Monoβ‡’Total = Monoβ‡’fβ†“β‰ˆid

  ∘-pres-total : {A B C : Obj} {f : B β‡’ C} {g : A β‡’ B} β†’ total f β†’ total g β†’ total (f ∘ g)
  ∘-pres-total {f = f} {g = g} tf tg = begin
    (f ∘ g) ↓   β‰ˆΛ˜βŸ¨ ↓-denestΛ‘ ⟩
    (f ↓ ∘ g) ↓ β‰ˆβŸ¨ ↓-cong (elimΛ‘ tf) ⟩
    g ↓         β‰ˆβŸ¨ tg ⟩
    id ∎

  total-gfβ‡’total-f : total (g ∘ f) β†’ total f
  total-gf⇒total-f {g = g} {f = f} tgf = begin
    f ↓             β‰ˆβŸ¨ introΚ³ tgf ⟩
    f ↓ ∘ (g ∘ f) ↓ β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
    (g ∘ f) ↓       β‰ˆβŸ¨ tgf ⟩
    id              ∎

  total-SubCat : SubCat π’ž Obj
  total-SubCat = record
    { U = Ξ» x β†’ x
    ; R = total
    ; Rid = Monoβ‡’Total (Mono-id π’ž)
    ; _∘R_ = ∘-pres-total
    }

  Total : Category o (β„“ βŠ” e) e
  Total = SubCategory π’ž total-SubCat