Lemma is_nat_trans_δ_comp_mor : is_nat_trans (δ_source (functor_compose G1 G2)) (δ_target (functor_compose G1 G2)) δ_comp_mor. Proof. intros Ze Z'e' αX; induction Ze as [Z e]; induction Z'e' as [Z' e']; induction αX as [α X]; simpl in *. apply nat_trans_eq; [apply homset_property |]; intro c; simpl. rewrite !id_right, !id_left. generalize (nat_trans_eq_pointwise (nat_trans_ax (δ G1 DL1) (Z,,e) (Z',, e') (α,,X)) c). generalize (nat_trans_eq_pointwise (nat_trans_ax (δ G2 DL2) (Z,,e) (Z',, e') (α,,X)) (G1 c)). intros Hyp1 Hyp2. cbn in Hyp1, Hyp2. etrans. 2: { rewrite <- assoc. apply maponpaths. exact Hyp1. } clear Hyp1. etrans. { rewrite assoc. apply cancel_postcomposition. apply pathsinv0, functor_comp. } etrans. { apply cancel_postcomposition. apply maponpaths. exact Hyp2. } rewrite (functor_comp G2). apply assoc'. 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.