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

open import Categories.Category
import Categories.Morphism.Reasoning

-- Lifting Properties
module Categories.Morphism.Lifts {o β„“ e} (π’ž : Category o β„“ e) where

open import Level

open Category π’ž
open Definitions π’ž
open Categories.Morphism.Reasoning π’ž using (pullΛ‘)

-- A pair of morphisms has the lifting property if every commutative
-- square admits a diagonal filler. We say that 'i' has the left lifting
-- property with respect to 'p', and that 'p' has the right lifting property
-- with respect to 'i'.
--
-- Graphically, the situation is as follows:
--
--      f
--   A ────> X
--   β”‚     ^ β”‚
--   β”‚  βˆƒ β•±  β”‚
-- i β”‚   β•±   β”‚ p
--   β”‚  β•±    β”‚
--   V β•±     V
--   B ────> Y
--      g
--
-- Note that the filler is /not/ required to be unique.
--
-- For ease of use, we define lifts in two steps:
-- * 'Filler' describes the data required to fill a /particular/ commutative square.
-- * 'Lifts' then quantifies over all commutative squares.

record Filler {A B X Y} {i : A β‡’ B} {f : A β‡’ X} {g : B β‡’ Y} {p : X β‡’ Y}
              (comm : CommutativeSquare i f g p) : Set (β„“ βŠ” e) where
  field
    filler : B β‡’ X
    fill-commΛ‘ : filler ∘ i β‰ˆ f
    fill-commΚ³ : p ∘ filler β‰ˆ g

Lifts : βˆ€ {A B X Y} β†’ (i : A β‡’ B) β†’ (p : X β‡’ Y) β†’ Set (β„“ βŠ” e)
Lifts i p = βˆ€ {f g} β†’ (comm : CommutativeSquare i f g p) β†’ Filler comm
-- The diagonal in a square. The record does not require the square to commute
-- but rather deduces this from the existence of the diagonal.
-- The reason is that if the record is parametrized by a morphism equality,
-- then record types differ if there are multiple (unequal) proofs of
-- morphism equality. Then, properties like FactorizationSystem.diag-uniqueβ‚‚
-- would become more complicated. Thus, Diagonal does not use
-- above Filler record, which is parametric in a morphism equality.
record Diagonal {A B C D} (i : A β‡’ B) (f : A β‡’ C)
                (g : B β‡’ D) (p : C β‡’ D) : Set (β„“ βŠ” e) where
  field
    --      i
    --   A ────> B
    --   β”‚     / β”‚
    --   β”‚  d β•±  β”‚
    -- f β”‚   β•±   β”‚ g
    --   β”‚  β•±    β”‚
    --   V V     V
    --    C ───> D
    --      m
    d : B β‡’ C
    commΛ‘ : d ∘ i β‰ˆ f
    commΚ³ : p ∘ d β‰ˆ g

  comm : CommutativeSquare i f g p
  comm = begin
    g ∘ i      β‰ˆβŸ¨ pullΛ‘ commΚ³ ⟨
    p ∘ d ∘ i  β‰ˆβŸ¨ refl⟩∘⟨ commΛ‘ ⟩
    p ∘ f      ∎
    where open HomReasoning

  toFiller : Filler comm
  toFiller = Filler.constructor d commΛ‘ commΚ³

Fillerβ‡’Diagonal : βˆ€ {A B X Y} {i : A β‡’ B} {f : A β‡’ X} {g : B β‡’ Y} {p : X β‡’ Y}
                  {comm : CommutativeSquare i f g p}
                  β†’ Filler comm
                  β†’ Diagonal i f g p
Filler⇒Diagonal f = record { d = filler ; commˑ = fill-commˑ ; commʳ = fill-commʳ }
  where open Filler f

record UniqueDiagonal {A B X Y} (i : A β‡’ B) (f : A β‡’ X)
                      (g : B β‡’ Y) (p : X β‡’ Y) : Set (β„“ βŠ” e) where
  field
    diagonal : Diagonal i f g p
  open Diagonal diagonal public
  field
    unique : βˆ€ (v : Diagonal i f g p) β†’ d β‰ˆ Diagonal.d v

  uniqueβ‚‚ : βˆ€ (v w : Diagonal i f g p) β†’ Diagonal.d v β‰ˆ Diagonal.d w
  uniqueβ‚‚ v w = begin
    Diagonal.d v  β‰ˆβŸ¨ unique v ⟨
    d             β‰ˆβŸ¨ unique w ⟩
    Diagonal.d w  ∎
    where open HomReasoning



--------------------------------------------------------------------------------
-- Lifings of Morphism Classes

-- Shorthand for denoting a class of morphisms.
MorphismClass : (p : Level) β†’ Set (o βŠ” β„“ βŠ” suc p)
MorphismClass p = βˆ€ {X Y} β†’ X β‡’ Y β†’ Set p

β‰ˆ-closed : {p : Level} β†’ (M : MorphismClass p) β†’ Set (o βŠ” β„“ βŠ” e βŠ” p)
β‰ˆ-closed M = βˆ€ {X Y} β†’ {f g : X β‡’ Y} β†’ f β‰ˆ g β†’ M f β†’ M g

-- Bundled structure for members of a morphism class
record MorphismClassMember {p : Level} (M : MorphismClass p) (A B : Obj) : Set (p βŠ” β„“) where
  field
    mor : A β‡’ B
    in-class : M mor

-- A morphism 'i' is called "projective" with respect to some morphism class 'J'
-- if it has the left-lifting property against every element of 'J'.
Projective : βˆ€ {j} {A B} β†’ MorphismClass j β†’ (i : A β‡’ B) β†’ Set (o βŠ” β„“ βŠ” e βŠ” j)
Projective J i = βˆ€ {X Y} β†’ (f : X β‡’ Y) β†’ J f β†’ Lifts i f

-- Dually, a morphism 'i' is called "injective" with repsect to a morphism class 'J'
-- if it has the right-lifting property against every element of 'J'.
Injective : βˆ€ {j} {A B} β†’ MorphismClass j β†’ (i : A β‡’ B) β†’ Set (o βŠ” β„“ βŠ” e βŠ” j)
Injective J i = βˆ€ {X Y} β†’ (f : X β‡’ Y) β†’ J f β†’ Lifts f i

-- The class of J-Projective morphisms.
Proj : βˆ€ {j} (J : MorphismClass j) β†’ MorphismClass (o βŠ” β„“ βŠ” e βŠ” j)
Proj J = Projective J

-- The class of J-Injective morphisms.
Inj : βˆ€ {j} (J : MorphismClass j) β†’ MorphismClass (o βŠ” β„“ βŠ” e βŠ” j)
Inj J = Injective J