∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} D]
  {X Y Z :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.WithTerminal.ofCommaMorphism (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.WithTerminal.ofCommaMorphism f)
      (CategoryTheory.WithTerminal.ofCommaMorphism g)