Lemma is_functor_BinProduct_of_functors_data : is_functor BinProduct_of_functors_data. Proof. split; simpl; intros. - red; intros; simpl in *. apply pathsinv0. unfold BinProduct_of_functors_mor. apply BinProduct_endo_is_identity. + rewrite BinProductOfArrowsPr1. rewrite functor_id. apply id_right. + rewrite BinProductOfArrowsPr2. rewrite functor_id. apply id_right. - red; intros; simpl in *. unfold BinProduct_of_functors_mor. do 2 rewrite functor_comp. apply pathsinv0. apply BinProductOfArrows_comp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.