Lemma is_nat_trans_δ_genoption_mor_nat_trans : is_nat_trans (δ_source genopt) (δ_target genopt) (λ Ze : Ptd, δ_genoption_mor Ze,, is_nat_trans_δ_genoption_mor Ze). Proof. intro Ze; induction Ze as [Z e]; intro Z'e'; induction Z'e' as [Z' e']; intro αX; induction αX as [α X]; simpl in *. apply nat_trans_eq; [apply homset_property |]; intro c; simpl. unfold BinCoproduct_of_functors_mor, BinCoproduct_of_functors_ob, δ_genoption_mor; simpl. rewrite precompWithBinCoproductArrow. apply pathsinv0, BinCoproductArrowUnique. - rewrite id_left, assoc. etrans. { apply cancel_postcomposition, BinCoproductIn1Commutes. } rewrite <- assoc. now apply maponpaths, X. - rewrite assoc. etrans. { apply cancel_postcomposition, BinCoproductIn2Commutes. } now apply nat_trans_ax. 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.