∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q R : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr))
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.Limits.coprod.desc
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl)
          CategoryTheory.Limits.coprod.inr)) =
    CategoryTheory.CategoryStruct.id ((P ⨿ Q) ⨿ R)