def CategoryTheory.MorphismProperty.llp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : MorphismProperty C

left lifting property with respect to a class of morphisms

Equations

• T.llp f = ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄, T g → CategoryTheory.HasLiftingProperty f g

def CategoryTheory.MorphismProperty.rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : MorphismProperty C

rlp wrt a class of morphisms

Equations

• T.rlp f = ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄, T g → CategoryTheory.HasLiftingProperty g f