Tom de Jong, 22 May 2025

An anonymous reviewer of our TYPES abstract [1] suggested that some of our
results could be generalized to weak factorization systems. Here we consider a
factorization system based on embeddings and maps whose fibers are all injective
types. We are also thinking about the connections to *algebraic* weak
factorization systems.

[1] Tom de Jong and Martı́n Hâtzel Escardó.
    "Examples and counter-examples of injective types in univalent mathematics".
    Abstract for the 31st International Conference on Types for Proofs and
    Programs (TYPES). 2025.
    url: https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper6.pdf.

\begin{code}

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

open import UF.FunExt

module InjectiveTypes.WeakFactorizationSystem
        (fe : FunExt)
       where

open import InjectiveTypes.Blackboard fe

open import MLTT.Spartan

open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.IdEmbedding
open import UF.Univalence

\end{code}

We define a fiberwise algebraically injective map to be one whose fibers are all
algebraically injective types.

NB. It may be that fiberwise flabbiness is more convenient to work with.

\begin{code}

fiberwise-ainjective : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ (A β†’ B) β†’ (𝓦 𝓣 : Universe)
                     β†’ ((𝓦 βŠ” 𝓣) ⁺ βŠ” 𝓀 βŠ” π“₯) Μ‡
fiberwise-ainjective f 𝓦 𝓣 =
 each-fiber-of f (Ξ» F β†’ ainjective-type F 𝓦 𝓣)

\end{code}

Any map can be factored as an embedding followed by a fiberwise algebraically
injective map.

\begin{code}

embedding-fiberwise-ainjective-factorization
 : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
 β†’ is-univalent (𝓀 βŠ” π“₯)
 β†’ (f : A β†’ B)
 β†’ Ξ£ X κž‰ (𝓀 βŠ” π“₯)⁺ Μ‡  ,
   Ξ£ l κž‰ (A β†’ X) ,
   Ξ£ r κž‰ (X β†’ B) , (f ＝ r ∘ l)
                 Γ— is-embedding l
                 Γ— fiberwise-ainjective r (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
embedding-fiberwise-ainjective-factorization {𝓀} {π“₯} {A} {B} ua f =
 X , l , r , refl , l-is-embedding ua , r-fiberwise-ainjective ua
  where
   X : (𝓀 βŠ” π“₯) ⁺ Μ‡
   X = Ξ£ b κž‰ B , (fiber f b β†’ (𝓀 βŠ” π“₯) Μ‡ )

   ΞΉ : (Y : 𝓀' Μ‡ ) β†’ Y β†’ (Y β†’ 𝓀' Μ‡ )
   ΞΉ Y = Id

   ΞΉ-is-embedding : is-univalent 𝓀' β†’ (Y : 𝓀' Μ‡ ) β†’ is-embedding (ΞΉ Y)
   ΞΉ-is-embedding ua _ = UA-Id-embedding ua fe

   l : A β†’ X
   l = NatΞ£ (Ξ» b β†’ ΞΉ (fiber f b)) ∘ ⌜ domain-is-total-fiber f ⌝

   l-is-embedding : is-univalent (𝓀 βŠ” π“₯) β†’ is-embedding l
   l-is-embedding ua =
    ∘-is-embedding
     (equivs-are-embeddings' (domain-is-total-fiber f))
     (NatΞ£-is-embedding
       (fiber f)
       (Ξ» b β†’ fiber f b β†’ 𝓀 βŠ” π“₯ Μ‡ )
       (Ξ» b β†’ ΞΉ (fiber f b))
       (Ξ» b β†’ ΞΉ-is-embedding ua (fiber f b)))

   r : X β†’ B
   r = pr₁

   r-fiberwise-ainjective : is-univalent (𝓀 βŠ” π“₯)
                          β†’ fiberwise-ainjective r (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
   r-fiberwise-ainjective ua b =
    equiv-to-ainjective
     (fiber r b)
     (fiber f b β†’ 𝓀 βŠ” π“₯ Μ‡ )
     (power-of-ainjective (universes-are-ainjective-Ξ ' ua))
     (pr₁-fiber-equiv b)

\end{code}

We have (specified) diagonal lifts of embeddings against fiberwise algebraically
injective maps.

We consider a commutative square with j an embedding and r fiberwise
algebraically injective and we look to find diagonal filler: a map e : Y β†’ D
making the resulting triangles commute.

       f
  X ------> D
  |       ^ |
  |      /  |
j |  βˆƒe /   | r
  |    /    |
  |   /     |
  v  /      v
  Y ------> E
       g

Note that in our case we have a designated filler.

\begin{code}

module lifting-problem
        {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {D : 𝓦 Μ‡ } {E : 𝓣 Μ‡ }
        (j : X β†’ Y) (f : X β†’ D) (r : D β†’ E) (g : Y β†’ E)
        (j-is-embedding : is-embedding j)
        (r-fiberwise-ainjective : fiberwise-ainjective r (𝓀 βŠ” π“₯) 𝓣')
        -- NB. The last universe parameter is arbitrary.
        (comm-sq : r ∘ f ∼ g ∘ j)
       where

 lifting-problem-has-a-solution : Ξ£ eΒ κž‰ (Y β†’ D) , (e ∘ j ∼ f) Γ— (r ∘ e ∼ g)
 lifting-problem-has-a-solution = e , e-upper-triangle , e-lower-triangle
  where
   module _ (y : Y) where

    fΜ… : fiber j y β†’ fiber r (g y)
    fΜ… (x , e) = (f x , (r (f x) ＝⟨ comm-sq x ⟩
                        g (j x) ＝⟨ ap g e ⟩
                        g y     ∎))

    𝕖 : Ξ£ e κž‰ fiber r (g y) , ((p : fiber j y) β†’ e ＝ fΜ… p)
    𝕖 = ainjective-types-are-aflabby
         (fiber r (g y))
         (r-fiberwise-ainjective (g y))
         (fiber j y)
         (j-is-embedding y)
         fΜ…

    eΚΈ = pr₁ 𝕖
    eΚΈ-extends : (p : fiber j y) β†’ eΚΈ ＝ fΜ… p
    eΚΈ-extends = prβ‚‚ 𝕖

   e : Y β†’ D
   e y = pr₁ (eΚΈ y)

   e-lower-triangle : r ∘ e ∼ g
   e-lower-triangle y = prβ‚‚ (eΚΈ y)

   e-upper-triangle : e ∘ j ∼ f
   e-upper-triangle x = ap pr₁ I
    where
     I : eΚΈ (j x) ＝ fΜ… (j x) (x , refl)
     I = eΚΈ-extends (j x) (x , refl)

\end{code}

In the above it is important to work with *algebraically* injective types: if we
instead had assumed that each fiber of r is only injective, then we would have
gotten for each y : Y an unspecified element of D only, which, in the absence of
choice, fails to produce a function.

Finally, since propositions and injective types are closed under retracts and
because retractions of maps induce retractions of their fibers [HoTTBook,
Lemma 4.7.3], the embeddings and the fiberwise injective maps are closed under
retracts, so that by the "retract argument" [Rie14, Lemma 11.2.3], the
embeddings and fiberwise injective maps indeed give rise to a weak factorization
system.

TODO. Formalize this and, as a preliminary, retracts of maps.

[Rie14] Emily Riehl. Categorical Homotopy Theory.
        New Mathematical Monographs 24.
        Cambridge University Press, 2014.
        doi: 10.1017/ CBO9781107261457.
        url: https://math.jhu.edu/~eriehl/cathtpy.pdf.