Theorem functorBinaryProduct {B C:category} : BinaryProducts C -> BinaryProducts [B,C]. Proof. intros prod F G. unshelve refine (z_iso_Representation_weq _ _). { exact (bifunctor_assoc (binaryProductFunctor F G)). } { now apply BinaryProductFunctorAssoc. } { apply bifunctor_assoc_repn. intro b. apply prod. } 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.