Definition sum_of_nat_trans_inl {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) : pre_whisker (inl_functor_data _ _) (sum_of_nat_trans α β) = α.
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.