∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [inst_3 : HomotopicalAlgebra.IsFibrant X]
  [inst_4 : HomotopicalAlgebra.IsFibrant Y] [inst_5 : HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : HomotopicalAlgebra.FibrantObject C} (h : HomotopicalAlgebra.FibrantObject.mk Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk g) h) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g))
      h