# Mere lifting properties

Content created by Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2023-02-18.

module orthogonal-factorization-systems.mere-lifting-properties where

Imports
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.universe-levels

open import orthogonal-factorization-systems.pullback-hom


## Idea

Given two maps, f : A → X and g : B → Y, we say that f has the mere left lifting property with respect to g and that g has the mere right lifting property with respect to f if the pullback-hom is surjective. This means that the type of lifting operations between f and g is merely inhabited.

## Definition

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

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


## Properties

### Mere lifting properties are properties

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

is-prop-mere-diagonal-lift : is-prop (mere-diagonal-lift f g)
is-prop-mere-diagonal-lift = is-prop-is-surjective (pullback-hom f g)

mere-diagonal-lift-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
mere-diagonal-lift-Prop = is-surjective-Prop (pullback-hom f g)