English
If φ and ψ are strongly cocartesian over g and f ≫ g respectively, and f φ is liftable, then φ is strongly cocartesian.
Русский
Если φ и ψ сильно кокартезианские над g и f ≫ g соответственно, и fφ поднимаема, тогда φ является сильно кокартезианским.
LaTeX
$$$[IsStronglyCartesian p g ψ] [IsStronglyCartesian p (f \\gg g) (φ \\gg ψ)] [IsHomLift p f φ] \\Rightarrow IsStronglyCartesian p f φ$$$
Lean4
/-- Given a co-Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a ⟶ b'` which also lifts `f`. Then any morphism `ψ : b ⟶ b'` lifting `𝟙 S` such that
`g ≫ ψ = φ'` must equal the map induced by the universal property of `φ`. -/
theorem map_uniq (ψ : b ⟶ b') [IsHomLift p (𝟙 S) ψ] (hψ : φ ≫ ψ = φ') : ψ = IsCocartesian.map p f φ φ' :=
(Classical.choose_spec <| IsCocartesian.universal_property (p := p) (f := f) (φ := φ) φ').2 ψ ⟨inferInstance, hψ⟩
