Lemma is_precategory_hss : is_precategory hss_precategory_data. Proof. apply is_precategory_one_assoc_to_two. repeat split; intros. - apply (invmap (hssMor_eq _ _ _ _ )). apply (@id_left EndC). - apply (invmap (hssMor_eq _ _ _ _ )). apply (@id_right EndC). - apply (invmap (hssMor_eq _ _ _ _ )). apply (@assoc EndC). 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.