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

open import Categories.Category.Core using (Category)
open import Categories.Category using (module Definitions)
open import Categories.Morphism.Lifts using (MorphismClass)


-- Consider a category π’ž and two morphism classes β„° and β„³.
-- The level of the morphism equalities is called `eq`
-- such that the identifier `e` stays fresh for members of β„°.
module Categories.Morphism.FactorizationSystem.Core
       {o β„“ eq} (π’ž : Category o β„“ eq)
       {β„“β„° β„“β„³} (β„° : MorphismClass π’ž β„“β„°) (β„³ : MorphismClass π’ž β„“β„³) where

open import Level

open import Categories.Morphism.Lifts π’ž using (MorphismClassMember; β‰ˆ-closed; UniqueDiagonal; Diagonal)
open import Categories.Morphism {o} {β„“} {eq} π’ž using (IsIso)
open Category π’ž
open Definitions π’ž using (CommutativeSquare)
open MorphismClassMember using (mor)

private
  variable
    A B C D : Obj

-- We write ->> / β†  for morphisms in β„°
_β† _ : Obj β†’ Obj β†’ Set (β„“ βŠ” β„“β„°)
_β† _ = MorphismClassMember β„°

-- We write >-> / ↣ for morphisms in β„³
_↣_ : Obj β†’ Obj β†’ Set (β„“ βŠ” β„“β„³)
_↣_ = MorphismClassMember β„³

record Factorization (h : A β‡’ B) : Set (o βŠ” β„“ βŠ” eq βŠ” β„“β„° βŠ” β„“β„³) where
  field
    Im : Obj
    e : A β†  Im
    m : Im ↣ B
    m∘eβ‰ˆh : mor m ∘ mor e β‰ˆ h

-- A factorization system (also called factorization structure) for
-- morphisms in the category π’ž, see section 14 of "Abstract and
-- Concrete Categories - The Joy of Cats" by AdΓ‘mek, Herrlich, Strecker, 2004.
record FactorizationSystem : Set (o βŠ” β„“ βŠ” eq βŠ” β„“β„° βŠ” β„“β„³) where
  field
    β„°-resp-β‰ˆ : β‰ˆ-closed β„°
    β„³-resp-β‰ˆ : β‰ˆ-closed β„³
    -- 1. every morphism admits an (β„°,β„³)-factorization
    factor : βˆ€ (f : A β‡’ B) β†’ Factorization f
    -- 2. β„° and β„³ are closed under compositions with isomorphisms:
    Isoβˆ˜β„° : βˆ€ {h : B β‡’ C} β†’ IsIso h β†’ (e : A β†  B) β†’ β„° (h ∘ mor e)
    β„³βˆ˜Iso : βˆ€ (m : B ↣ C) β†’ {h : A β‡’ B} β†’ IsIso h β†’ β„³ (mor m ∘ h)
    -- 3. every commutative square of the form
    --      e
    --   A ───>> B
    --   β”‚     / β”‚
    --   β”‚  βˆƒ!β•±  β”‚
    -- f β”‚   β•±   β”‚ g
    --   β”‚  β•±    β”‚
    --   V V     V
    --    C >──> D
    --      m
    --  has a unique diagonal filler.
    diagonal-filler : {f : A β‡’ C} {g : B β‡’ D} (e : A β†  B) (m : C ↣ D)
                      (comm : CommutativeSquare (mor e) f g (mor m))
                      β†’ UniqueDiagonal (mor e) f g (mor m)
  diag-uniqueβ‚‚ : {f : A β‡’ C} {g : B β‡’ D} (e : A β†  B) (m : C ↣ D)
            β†’ (d₁ dβ‚‚ : Diagonal (mor e) f g (mor m))
            β†’ Diagonal.d d₁ β‰ˆ Diagonal.d dβ‚‚
  diag-uniqueβ‚‚ {f = f} {g = g} e m d₁ dβ‚‚ =
    UniqueDiagonal.uniqueβ‚‚ (diagonal-filler e m (Diagonal.comm d₁)) d₁ dβ‚‚