∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' R'' : 𝒮} {a' a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'}
  (H : f' = CategoryTheory.CategoryStruct.comp g f) (H' : f'' = CategoryTheory.CategoryStruct.comp g' f') (φ' : a' ⟶ b)
  (φ'' : a'' ⟶ b) [inst_3 : p.IsStronglyCartesian f' φ'] [inst_4 : p.IsHomLift f'' φ''],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'')
      (CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ') =
    CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ''