Lifting operations
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2023-02-18.
Last modified on 2023-09-11.
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
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-08-23. Fredrik Bakke. Pre-commit fixes and some miscellaneous changes (#705).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622).