Definition δ_comp_mor (Ze : ptd_obj C) : [C, C] ⟦pr1 (δ_source (functor_compose G1 G2)) Ze, pr1 (δ_target (functor_compose G1 G2)) Ze⟧. Proof. set (Z := pr1 Ze). set (F1 := lassociator_CAT Z G1 G2). set (F2 := rwhisker_CAT G2 (δ G1 DL1 Ze)). set (F3 := rassociator_CAT G1 Z G2). set (F4 := lwhisker_CAT G1 (δ G2 DL2 Ze)). set (F5 := lassociator_CAT G1 G2 Z). exact (F1 · (F2 · (F3 · (F4 · F5)))). Defined.
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.