∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr
      (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv =
    CategoryTheory.Limits.coprod.inr