proposition: Lemma is_functor_hcomp : is_functor hcomp_functor_data.
proof: Proof. split; red; cbn. - intros (f1, f2). cbn. apply hcomp_identity. - intros (f1, f2) (g1, g2) (h1, h2). unfold precategory_binproduct_mor. cbn. intros (x1, x2) (y1, y2). cbn. apply hcomp_vcomp. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct