∀ {𝒮 : 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} [self : p.IsCocartesian f φ],
  p.IsHomLift f φ