open import Cat.Diagram.Coproduct.Copower
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Functor.Morphism
open import Cat.Diagram.Zero
open import Cat.Functor.Hom
open import Cat.Prelude

open import Data.Set.Projective
open import Data.Set.Surjection
open import Data.Dec

import Cat.Diagram.Separator.Strong
import Cat.Diagram.Projective
import Cat.Morphism.StrongEpi
import Cat.Reasoning

module Cat.Diagram.Projective.Strong
  {o β„“}
  (C : Precategory o β„“)
  where

open Cat.Diagram.Projective C
open Cat.Morphism.StrongEpi C
open Cat.Reasoning C

Strong projective objectsπŸ”—

Let be a precategory. An object is a strong projective object if it has the left-lifting property against strong epimorphisms.

More explicitly, is a strong projective object if for every morphism and strong epi there merely exists a such that as in the following diagram:

is-strong-projective : (P : Ob) β†’ Type _
is-strong-projective P =
  βˆ€ {X Y} (p : Hom P Y) (e : Hom X Y)
  β†’ is-strong-epi e
  β†’ βˆƒ[ s ∈ Hom P X ] (e ∘ s ≑ p)
\ Warning

Being a strong projective object is actually a weaker condition than being a projective object: strong projectives only need to lift against strong epis, whereas projectives need to lift against all epis.

projective→strong-projective
  : βˆ€ {P}
  β†’ is-projective P
  β†’ is-strong-projective P
projective→strong-projective pro p e e-strong =
  pro p (record { mor = e ; epic = e-strong .fst })

A functorial definitionπŸ”—

Like their non-strong counterparts, we can give a functorial definition of strong projectives. In particular, an object is a strong projective if and only if the preserves strong epimorphisms.

preserves-strong-epis→strong-projective
  : βˆ€ {P}
  β†’ preserves-strong-epis (Hom-from C P)
  β†’ is-strong-projective P

strong-projective→preserves-strong-epis
  : βˆ€ {P}
  β†’ is-strong-projective P
  β†’ preserves-strong-epis (Hom-from C P)
These proofs are essentially the same as the corresponding ones for projective objects, so we omit the details. 
preserves-strong-epis→strong-projective {P = P} hom-epi {X = X} {Y = Y} p e e-strong =
  epi→surjective (el! (Hom P X)) (el! (Hom P Y))
    (e ∘_)
    (Ξ» {c} β†’ hom-epi e-strong .fst {c = c})
    p

strong-projective→preserves-strong-epis {P = P} pro {X} {Y} {f = f} f-strong =
    surjectiveβ†’strong-epi (el! (Hom P X)) (el! (Hom P Y)) (f ∘_) $ Ξ» p β†’
    pro p f f-strong

Closure of strong projectivesπŸ”—

Like projective objects, strong projectives are closed under coproducts indexed by set-projective types and retracts.

indexed-coproduct-strong-projective
  : βˆ€ {ΞΊ} {Idx : Type ΞΊ}
  β†’ {P : Idx β†’ Ob} {∐P : Ob} {ΞΉ : βˆ€ i β†’ Hom (P i) ∐P}
  β†’ is-set-projective Idx β„“
  β†’ (βˆ€ i β†’ is-strong-projective (P i))
  β†’ is-indexed-coproduct C P ΞΉ
  β†’ is-strong-projective ∐P

retract→strong-projective
  : βˆ€ {R P}
  β†’ is-strong-projective P
  β†’ (s : Hom R P)
  β†’ has-retract s
  β†’ is-strong-projective R
These proofs are more or less identical to the corresponding ones for projective objects. 
indexed-coproduct-strong-projective {P = P} {ΞΉ = ΞΉ} Idx-pro P-pro coprod {X = X} {Y = Y} p e e-strong = do
  s ← Idx-pro
        (Ξ» i β†’ Ξ£[ sα΅’ ∈ Hom (P i) X ] (e ∘ sα΅’ ≑ p ∘ ΞΉ i)) (Ξ» i β†’ hlevel 2)
        (Ξ» i β†’ P-pro i (p ∘ ΞΉ i) e e-strong)
  pure (match (Ξ» i β†’ s i .fst) , uniqueβ‚‚ (Ξ» i β†’ pullr commute βˆ™ s i .snd))
  where open is-indexed-coproduct coprod

retract→strong-projective P-pro s r p e e-strong = do
  (t , t-factor) ← P-pro (p ∘ r .retract) e e-strong
  pure (t ∘ s , pulll t-factor βˆ™ cancelr (r .is-retract))

Moreover, if has a zero object and a strong projective coproduct indexed by a discrete type, then each component of the coproduct is a strong projective.

zero+indexed-coproduct-strong-projective→strong-projective
  : βˆ€ {ΞΊ} {Idx : Type ΞΊ} ⦃ Idx-Discrete : Discrete Idx ⦄
  β†’ {P : Idx β†’ Ob} {∐P : Ob} {ΞΉ : βˆ€ i β†’ Hom (P i) ∐P}
  β†’ Zero C
  β†’ is-indexed-coproduct C P ΞΉ
  β†’ is-strong-projective ∐P
  β†’ βˆ€ i β†’ is-strong-projective (P i)
Following the general theme, the proof is identical to the non-strong case. 
zero+indexed-coproduct-strong-projectiveβ†’strong-projective {ΞΉ = ΞΉ} z coprod ∐P-pro i =
  retractβ†’strong-projective ∐P-pro (ΞΉ i) $
  zero→ι-has-retract C coprod z i

Enough strong projectivesπŸ”—

A category is said to have enough strong projectives if for object there is some strong epi with strong projective. We will refer to these projectives as projective presentations of

Note that there are two variations on this condition: one where there merely exists a strong projective presentation for every and another where those presentations are provided as structure. We prefer to work with the latter, as it tends to be less painful to work with.

record Strong-projectives : Type (o βŠ” β„“) where
  field
    Pro : Ob β†’ Ob
    present : βˆ€ {X} β†’ Hom (Pro X) X
    present-strong-epi : βˆ€ {X} β†’ is-strong-epi (present {X})
    projective : βˆ€ {X} β†’ is-strong-projective (Pro X)

module _ (coprods : (Idx : Set β„“) β†’ has-coproducts-indexed-by C ∣ Idx ∣)
  where
  open Cat.Diagram.Separator.Strong C coprods
  open Copowers coprods

If has set-indexed coproducts, and is a strong separating family with each a strong projective, then has enough strong projectives if is a set-projective type.

  strong-projective-separating-faily→strong-projectives
    : βˆ€ {Idx : Set β„“} {Pα΅’ : ∣ Idx ∣ β†’ Ob}
    β†’ (βˆ€ X β†’ is-set-projective (Ξ£[ i ∈ ∣ Idx ∣ ] (Hom (Pα΅’ i) X)) β„“)
    β†’ (βˆ€ i β†’ is-strong-projective (Pα΅’ i))
    β†’ is-strong-separating-family Idx Pα΅’
    β†’ Strong-projectives

The hypotheses of this theorem basically give the game away: by definition, there is a strong epimorphism for every Moreover, is set-projective, so the corresponding coproduct is a strong projective.

  strong-projective-separating-faily→strong-projectives
    {Idx} {Pα΅’} Idx-pro Pα΅’-pro strong-sep = strong-projectives where
    open Strong-projectives

    strong-projectives : Strong-projectives
    strong-projectives .Pro X =
      ∐! (Ξ£[ i ∈ ∣ Idx ∣ ] (Hom (Pα΅’ i) X)) (Pα΅’ βŠ™ fst)
    strong-projectives .present {X = X} =
      ∐!.match (Ξ£[ i ∈ ∣ Idx ∣ ] (Hom (Pα΅’ i) X)) (Pα΅’ βŠ™ fst) snd
    strong-projectives .present-strong-epi =
      strong-sep
    strong-projectives .projective {X = X} =
      indexed-coproduct-strong-projective
        (Idx-pro X)
        (Pα΅’-pro βŠ™ fst)
        (∐!.has-is-ic (Ξ£[ i ∈ ∣ Idx ∣ ] (Hom (Pα΅’ i) X)) (Pα΅’ βŠ™ fst))