Lemma ishssMor_id (T : hss) : ishssMor (identity (C:=category_FunctorAlg _) (pr1 T)). Proof. unfold ishssMor. unfold isbracketMor. intros Z f. rewrite id_right. rewrite functor_id. rewrite id_right. apply pathsinv0. set (H2:=pre_composition_functor _ _ C (U Z)). set (H2' := functor_id H2). simpl in H2'. simpl. rewrite H2'. rewrite (@id_left EndC). apply idpath. 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.