proposition: Lemma is_nat_trans_θ_from_δ_mor : is_nat_trans (θ_source precompG) (θ_target precompG) θ_from_δ_mor.
proof: Proof. intros H1 H2 αη; induction H1 as [F1 Ze1]; induction H2 as [F2 Ze2]; induction αη as [α η]. apply nat_trans_eq_alt; intro c. simpl; rewrite !id_right, !id_left. generalize (nat_trans_eq_pointwise (nat_trans_ax (δ G DL) Ze1 Ze2 η) c); simpl. intro H. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply functor_comp. } etrans. 2: { apply cancel_postcomposition. apply maponpaths. exact H. } clear H. rewrite functor_comp. do 2 rewrite <- assoc. apply maponpaths. apply pathsinv0, nat_trans_ax. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.PointedFunctors UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.PointedFunctorsComposition