∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c)
  [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ]
  [inst_3 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Fiber.homMk p S φ)
      (CategoryTheory.Functor.Fiber.homMk p S ψ) =
    CategoryTheory.Functor.Fiber.homMk p S (CategoryTheory.CategoryStruct.comp φ ψ)