proposition: Lemma ishssMor_comp {T T' T'' : hss} (β : hssMor T T') (γ : hssMor T' T'') : ishssMor (compose (C:=category_FunctorAlg _) (pr1 β) (pr1 γ)).
proof: 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. do 2 rewrite functor_comp. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, (functor_comp (pre_composition_functor _ _ C (U Z)) ). Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation