CategoryTheory.HasLiftingProperty.sq_hasLift

theorem CategoryTheory.HasLiftingProperty.sq_hasLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} [self : CategoryTheory.HasLiftingProperty i p] {f : A ⟶ X} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift

The theorem `CategoryTheory.HasLiftingProperty.sq_hasLift` states that for any given category `C` with objects `A`, `B`, `X`, `Y`, morphisms `i : A ⟶ B` and `p : X ⟶ Y`, and provided that the morphism `i` has the lifting property with respect to `p`, then for any commutative square built from `f : A ⟶ X` and `g : B ⟶ Y`, there exists a lift. In other words, in this category, any commutative square constructed with these morphisms will satisfy the lifting property.

More concisely: Given any commutative square in a category where the inner rectangle has the lifting property, there exists a lift.