English
Let g: Z → W and t: Y → W define a pullback diagram. If p: X → Y has the lifting property with respect to t, and a pullback exists for g and t, then p has the lifting property with respect to the projection fst: pullback(g, t) → Z. In other words, every commutative square with left side p and right side fst can be lifted.
Русский
Пусть g: Z → W и t: Y → W образуют диаграмму-перелом, и существует вытягивание. Если p: X → Y имеет свойство подъёма относительно t, и существует проекция fst из вытянутого произведения pullback(g, t) на Z, то p имеет свойство подъёма относительно fst. То есть для любой коммутативной квадраты с левой гранью p и правой гранью fst существует диагональное витие.
LaTeX
$$$[HasPullback(g,t)] \\wedge [HasLiftingProperty(p,t)] \\Rightarrow HasLiftingProperty(p, \\text{pullback.fst}(g,t)).$$$
Lean4
instance [HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty p t] :
HasLiftingProperty p (pullback.fst g t) :=
(IsPullback.of_hasPullback g t).flip.hasLiftingProperty p
