Lemma is_nat_trans_δ_genoption_mor (Ze : Ptd) : is_nat_trans (δ_source genopt Ze : functor C C) (δ_target genopt Ze : functor C C) (δ_genoption_mor Ze). Proof. intros a b f; simpl. induction Ze as [Z e]. unfold BinCoproduct_of_functors_mor; simpl. etrans. { apply precompWithBinCoproductArrow. } rewrite id_left. apply pathsinv0, BinCoproductArrowUnique. - etrans. { rewrite assoc. apply cancel_postcomposition, BinCoproductIn1Commutes. } rewrite <- assoc. etrans. { apply maponpaths, pathsinv0, (nat_trans_ax e). } simpl; rewrite assoc. apply cancel_postcomposition. etrans. { apply BinCoproductOfArrowsIn1. } now rewrite id_left. - rewrite assoc. etrans. { apply cancel_postcomposition, BinCoproductIn2Commutes. } rewrite <- !functor_comp. now apply maponpaths, BinCoproductOfArrowsIn2. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.PointedFunctorsComposition.