Definition functorial_composition_legacy_data (A B C : category) : functor_data (precategory_binproduct_data [A, B] [B, C]) [A, C]. Proof. exists (λ FG, functor_composite (pr1 FG) (pr2 FG)). intros a b αβ. exact (horcomp (pr1 αβ) (pr2 αβ)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.