Lemma is_nat_trans_Gθ_mor : is_nat_trans (θ_source GH) (θ_target GH) Gθ_mor. Proof. intros H1 H2 αX; induction H1 as [F1 X1]; induction H2 as [F2 X2]. apply nat_trans_eq_alt; intro c; simpl. do 2 rewrite id_left. rewrite <- assoc. etrans. { apply maponpaths, pathsinv0, functor_comp. } etrans. { apply pathsinv0, functor_comp. } apply pathsinv0; etrans. { apply pathsinv0, functor_comp. } apply maponpaths. apply pathsinv0. rewrite assoc. generalize (nat_trans_eq_pointwise (nat_trans_ax θ (F1,,X1) (F2,,X2) αX) c). intro Hyp. apply Hyp. 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.