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.

       ∙
      ^ \
     /   \
    /     v
  A -----> B
      f

Definition

Factorization operations

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

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