∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  {X Y Z :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))}
  (f : CategoryTheory.CommaMorphism X Y) (g : CategoryTheory.CommaMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left