def CategoryTheory.MorphismProperty.llp {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty C

rlp wrt a class of morphisms

Equations

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