English
Let p: X ⥤ S be a functor, and suppose f: R → S and φ: a → b are such that φ is strongly Cartesian over f. For any R' and a' with a morphism g: R' → R and f': R' → S satisfying f' = g ∘ f, and any φ': a' → b that lifts f', there exists a unique χ: a' → a such that χ is a lift of g along p and χ ∘ φ = φ'.
Русский
Пусть p: X ⥤ S – функтор, и пусть φ: a → b является сильно-Картезианским над f: R → S. Для любых R' и a' c существованием г: R' → R и f': R' → S с условием f' = g ∘ f, и для любого φ': a' → b, который является подъёмом f', существует единственный χ: a' → a такой, что χ является подъёмом g вдоль p и χ ∘ φ = φ'.
LaTeX
$$$\\forall R'\\ (a' : \\, 𝒳)\\ (g : R' \\to R)\\ (f' : R' \\to S)$ $\\big( hf' : f' = g \\circ f \\big)\\ (φ' : a' \\to b)\\,[IsHomLift(p,f',φ')]\\;\\exists!\\; χ : a' \\to a,\\; IsHomLift(p,g,χ) \\wedge χ \\circ φ = φ'.$$$
Lean4
/-- The universal property of a strongly Cartesian morphism.
This lemma is more flexible with respect to non-definitional equalities than the field
`universal_property'` of `IsStronglyCartesian`. -/
theorem universal_property {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S) (hf' : f' = g ≫ f) (φ' : a' ⟶ b)
[IsHomLift p f' φ'] : ∃! χ : a' ⟶ a, IsHomLift p g χ ∧ χ ≫ φ = φ' :=
by
subst_hom_lift p f' φ'; clear a b R S
have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ inferInstance)
apply IsStronglyCartesian.universal_property' f
