Lemma category_precategory_is_precategory : is_precategory category_precategory_data. Proof. use make_is_precategory_one_assoc; intros; apply (functor_eq _ _ (homset_property _)); now use functor_data_eq. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory.