Lemma mapdiagram_bincoproduct_eq_diag {C : category}{D : category} (F : functor C D)(a b : C) : eq_diag (C := D) (mapdiagram F (BinCoproducts.bincoproduct_diagram a b)) (BinCoproducts.bincoproduct_diagram (F a) (F b)). Proof. use tpair. - use bool_rect; apply idpath. - intros ??; use empty_rect. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.