Lifting operations

module orthogonal-factorization-systems.lifting-operations where

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.homotopies
open import foundation.sections
open import foundation.universe-levels

open import orthogonal-factorization-systems.pullback-hom

Idea

Given two maps, f : A → X and g : B → Y, a lifting operation between f and g is a choice of lifting square for every commuting square

  A ------> B
  |         |
 f|         |g
  |         |
  V         V
  X ------> Y.

Given a lifting operation we can say that f has a left lifting structure with respect to g and that g has a right lifting structure with respect to f.

Warning

This is the Curry–Howard interpretation of what is classically called lifting properties. However, these are generally additional structure on the maps.

For the proof-irrelevant notion see mere lifting properties.

Definition

We define lifting operations to be sections of the pullback-hom.

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

  diagonal-lift : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  diagonal-lift = sec (pullback-hom f g)

  _⧄_ = diagonal-lift -- This symbol doesn't have an input sequence :(

  map-diagonal-lift : diagonal-lift → type-pullback-hom f g → X → B
  map-diagonal-lift = pr1

  issec-map-diagonal-lift :
    (d : diagonal-lift) → (pullback-hom f g ∘ map-diagonal-lift d) ~ id
  issec-map-diagonal-lift = pr2