proposition: Lemma is_precategory_hss : is_precategory hss_precategory_data.
proof: 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.
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