Lifting operations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-02-18.
Last modified on 2024-04-25.

module orthogonal-factorization-systems.lifting-operations where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.morphisms-arrows
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
  ∨         ∨
  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.

Note: 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 = section (pullback-hom f g)

  _⧄_ = diagonal-lift

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

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

Recent changes