Theorem functorBinarySum {B C:category} : BinarySums C -> BinarySums [B,C]. Proof. intros sum F G. exact (isomorphismRepresentability (functorBinaryProduct (binarySumsToProducts sum) (functorOp F) (functorOp G)) functorOpIso (HomPairOp F G)). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.