# Factorizations of maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-10.

module orthogonal-factorization-systems.factorizations-of-maps where
Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-algebra
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.retracts-of-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

## Idea

A factorization of a map f : A → B is a pair of maps g : X → B and h : A → X such that their composite g ∘ h is f.

X
∧ \
h /   \ g
/     ∨
A -----> B
f

We use diagrammatic order and say the map h is the left and g the right map of the factorization.

## Definitions

### The predicate on triangles of maps of being a factorization

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)
where

is-factorization :
{l3 : Level} {X : UU l3}
(g : X  B) (h : A  X)  UU (l1  l2)
is-factorization g h = g  h ~ f

### The type of factorizations of a map through a specified image/type

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
where

factorization-through : (f : A  B) (X : UU l3)  UU (l1  l2  l3)
factorization-through f X =
Σ ( X  B)
( λ g
Σ ( A  X)
( is-factorization f g))

right-map-factorization-through :
{f : A  B} {X : UU l3}  factorization-through f X  X  B
right-map-factorization-through = pr1

left-map-factorization-through :
{f : A  B} {X : UU l3}  factorization-through f X  A  X
left-map-factorization-through = pr1  pr2

is-factorization-factorization-through :
{f : A  B} {X : UU l3}
(F : factorization-through f X)
is-factorization f
( right-map-factorization-through F)
( left-map-factorization-through F)
is-factorization-factorization-through = pr2  pr2

### The type of factorizations of a map through images in a universe

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

factorization : (l3 : Level) (f : A  B)  UU (l1  l2  lsuc l3)
factorization l3 f = Σ (UU l3) (factorization-through f)

image-factorization : {l3 : Level} {f : A  B}  factorization l3 f  UU l3
image-factorization = pr1

factorization-through-factorization :
{l3 : Level} {f : A  B} (F : factorization l3 f)
factorization-through f (image-factorization F)
factorization-through-factorization = pr2

right-map-factorization :
{l3 : Level} {f : A  B} (F : factorization l3 f)
image-factorization F  B
right-map-factorization F =
right-map-factorization-through (factorization-through-factorization F)

left-map-factorization :
{l3 : Level} {f : A  B} (F : factorization l3 f)
A  image-factorization F
left-map-factorization F =
left-map-factorization-through (factorization-through-factorization F)

is-factorization-factorization :
{l3 : Level} {f : A  B} (F : factorization l3 f)
is-factorization f (right-map-factorization F) (left-map-factorization F)
is-factorization-factorization F =
is-factorization-factorization-through
( factorization-through-factorization F)

## Properties

### Whiskering of factorizations by retracts

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)
where

whisker-image-factorization-through :
{l3 l4 : Level} {X : UU l3} {Y : UU l4}
X retract-of Y  factorization-through f X  factorization-through f Y
pr1 (whisker-image-factorization-through (s , r , h) (fr , fl , fH)) =
fr  r
pr1 (pr2 (whisker-image-factorization-through (s , r , h) (fr , fl , fH))) =
s  fl
pr2 (pr2 (whisker-image-factorization-through (s , r , h) (fr , fl , fH))) =
(fr ·l (h ·r fl)) ∙h fH

### Characterization of identifications of factorizations through a type

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B)
{X : UU l3}
where

coherence-htpy-factorization-through :
(F E : factorization-through f X)
right-map-factorization-through F ~ right-map-factorization-through E
left-map-factorization-through F ~ left-map-factorization-through E
UU (l1  l2)
coherence-htpy-factorization-through F E R L =
( is-factorization-factorization-through F) ~
( horizontal-concat-htpy R L ∙h is-factorization-factorization-through E)

htpy-factorization-through :
(F E : factorization-through f X)  UU (l1  l2  l3)
htpy-factorization-through F E =
Σ ( right-map-factorization-through F ~
right-map-factorization-through E)
( λ R
Σ ( left-map-factorization-through F ~
left-map-factorization-through E)
( coherence-htpy-factorization-through F E R))

refl-htpy-factorization-through :
(F : factorization-through f X)  htpy-factorization-through F F
pr1 (refl-htpy-factorization-through F) = refl-htpy
pr1 (pr2 (refl-htpy-factorization-through F)) = refl-htpy
pr2 (pr2 (refl-htpy-factorization-through F)) = refl-htpy

htpy-eq-factorization-through :
(F E : factorization-through f X)
F  E  htpy-factorization-through F E
htpy-eq-factorization-through F .F refl = refl-htpy-factorization-through F

is-torsorial-htpy-factorization-through :
(F : factorization-through f X)
is-torsorial (htpy-factorization-through F)
is-torsorial-htpy-factorization-through F =
is-torsorial-Eq-structure
( is-torsorial-htpy (right-map-factorization-through F))
( right-map-factorization-through F , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-htpy (left-map-factorization-through F))
( left-map-factorization-through F , refl-htpy)
( is-torsorial-htpy (is-factorization-factorization-through F)))

is-equiv-htpy-eq-factorization-through :
(F E : factorization-through f X)
is-equiv (htpy-eq-factorization-through F E)
is-equiv-htpy-eq-factorization-through F =
fundamental-theorem-id
( is-torsorial-htpy-factorization-through F)
( htpy-eq-factorization-through F)

extensionality-factorization-through :
(F E : factorization-through f X)
(F  E)  (htpy-factorization-through F E)
pr1 (extensionality-factorization-through F E) =
htpy-eq-factorization-through F E
pr2 (extensionality-factorization-through F E) =
is-equiv-htpy-eq-factorization-through F E

eq-htpy-factorization-through :
(F E : factorization-through f X)
htpy-factorization-through F E  F  E
eq-htpy-factorization-through F E =
map-inv-equiv (extensionality-factorization-through F E)

### Characterization of identifications of factorizations of a map in a universe level

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B)
where

equiv-factorization :
(F E : factorization l3 f)  UU (l1  l2  l3)
equiv-factorization F E =
Σ ( image-factorization F  image-factorization E)
( λ e
htpy-factorization-through f
( whisker-image-factorization-through f
( map-equiv e , retraction-map-equiv e)
( factorization-through-factorization F))
( factorization-through-factorization E))

id-equiv-factorization :
(F : factorization l3 f)  equiv-factorization F F
pr1 (id-equiv-factorization F) = id-equiv
pr2 (id-equiv-factorization F) =
refl-htpy-factorization-through f (factorization-through-factorization F)

equiv-eq-factorization :
(F E : factorization l3 f)
F  E  equiv-factorization F E
equiv-eq-factorization F .F refl = id-equiv-factorization F

is-torsorial-equiv-factorization :
(F : factorization l3 f)
is-torsorial (equiv-factorization F)
is-torsorial-equiv-factorization F =
is-torsorial-Eq-structure
( is-torsorial-equiv (image-factorization F))
( image-factorization F , id-equiv)
( is-torsorial-htpy-factorization-through f
( factorization-through-factorization F))

is-equiv-equiv-eq-factorization :
(F E : factorization l3 f)  is-equiv (equiv-eq-factorization F E)
is-equiv-equiv-eq-factorization F =
fundamental-theorem-id
( is-torsorial-equiv-factorization F)
( equiv-eq-factorization F)

extensionality-factorization :
(F E : factorization l3 f)  (F  E)  (equiv-factorization F E)
pr1 (extensionality-factorization F E) = equiv-eq-factorization F E
pr2 (extensionality-factorization F E) = is-equiv-equiv-eq-factorization F E

eq-equiv-factorization :
(F E : factorization l3 f)  equiv-factorization F E  F  E
eq-equiv-factorization F E = map-inv-equiv (extensionality-factorization F E)