Lemma is_nat_trans_θ_from_δ_mor : is_nat_trans (θ_source precompG) (θ_target precompG) θ_from_δ_mor. 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.
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.