This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Factorization operations

module orthogonal-factorization-systems.factorization-operations where

open import foundation.universe-levels

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

Idea

A factorization operation on a function type A → B is a choice of factorization for every map f in A → B.

      Im f
      ∧  \
     /    \
    /      ∨
  A ------> B
       f

Definition

Factorization operations

instance-factorization-operation :
  {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2 ⊔ lsuc l3)
instance-factorization-operation l3 A B = (f : A → B) → factorization l3 f

factorization-operation : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
factorization-operation l1 l2 l3 =
  {A : UU l1} {B : UU l2} → instance-factorization-operation l3 A B