# Lifting operations

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

Created on 2023-02-18.

module orthogonal-factorization-systems.lifting-operations where

Imports
open import foundation.dependent-pair-types
open import foundation.fibered-maps
open import foundation.function-types
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.

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 → fibered-map 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