Lemma ishssMor_comp {T T' T'' : hss} (β : hssMor T T') (γ : hssMor T' T'') : ishssMor (compose (C:=category_FunctorAlg _) (pr1 β) (pr1 γ)). Proof. unfold ishssMor. unfold isbracketMor. intros Z f. eapply pathscomp0; [apply assoc|]. etrans. { apply cancel_postcomposition. apply isbracketMor_hssMor. } rewrite <- assoc. etrans. { apply maponpaths. apply isbracketMor_hssMor. } rewrite assoc. rewrite functor_comp. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, (functor_comp (pre_composition_functor _ _ C (U Z)) ). Qed.
Require Import UniMath.Foundations.PartD. 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.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation.