# Factorization operations into function classes

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-09.

module orthogonal-factorization-systems.factorization-operations-function-classes where

Imports
open import foundation.contractible-types
open import foundation.function-types
open import foundation.inhabited-types
open import foundation.propositions
open import foundation.universe-levels

open import orthogonal-factorization-systems.factorizations-of-maps
open import orthogonal-factorization-systems.function-classes


## Idea

A factorization operation into function classes L and R is a factorization operation such that the left map (in diagrammatic order) of every factorization is in L, and the right map is in R.

       ∙
^ \
L ∋ /   \ ∈ R
/     v
A -----> B


## Definition

module _
{l1 l2 lF lL lR : Level}
(L : function-class l1 lF lL)
(R : function-class lF l2 lR)
(A : UU l1) (B : UU l2)
where

factorization-operation-function-class :
UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR)
factorization-operation-function-class =
(f : A → B) → factorization-function-class L R f

mere-factorization-property-function-class :
UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR)
mere-factorization-property-function-class =
(f : A → B) → is-inhabited (factorization-function-class L R f)

unique-factorization-operation-function-class :
UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR)
unique-factorization-operation-function-class =
(f : A → B) → is-contr (factorization-function-class L R f)


## Properties

### A mere function class factorization property is a property

module _
{l1 l2 lF lL lR : Level}
(L : function-class l1 lF lL)
(R : function-class lF l2 lR)
{A : UU l1} {B : UU l2}
where

mere-factorization-property-function-class-Prop :
Prop (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR)
mere-factorization-property-function-class-Prop =
Π-Prop (A → B) (is-inhabited-Prop ∘ factorization-function-class L R)

is-prop-mere-factorization-property-function-class :
is-prop (mere-factorization-property-function-class L R A B)
is-prop-mere-factorization-property-function-class =
is-prop-type-Prop mere-factorization-property-function-class-Prop


### Having a unique function class factorization operation is a property

module _
{l1 l2 lF lL lR : Level}
(L : function-class l1 lF lL)
(R : function-class lF l2 lR)
{A : UU l1} {B : UU l2}
where

unique-factorization-operation-function-class-Prop :
Prop (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR)
unique-factorization-operation-function-class-Prop =
Π-Prop (A → B) (is-contr-Prop ∘ factorization-function-class L R)

is-prop-unique-factorization-operation-function-class :
is-prop (unique-factorization-operation-function-class L R A B)
is-prop-unique-factorization-operation-function-class =
is-prop-type-Prop unique-factorization-operation-function-class-Prop