Definition sum_of_nat_trans_data {Q C₁ C₂ : category} {F G : bincoprod_of_category C₁ C₂ ⟶ Q} (α : inl_functor C₁ C₂ ∙ F ⟹ inl_functor C₁ C₂ ∙ G) (β : inr_functor C₁ C₂ ∙ F ⟹ inr_functor C₁ C₂ ∙ G) : nat_trans_data F G. Proof. intros z. induction z as [ x | y ]. - exact (α x). - exact (β y). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering.