∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] {X Y Z : C × CategoryTheory.Discrete PUnit.{u_2 + 1}}
  (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1