Definition cat_of_elems_data : precategory_data. Proof. exists cat_of_elems_ob_mor. split. + intros a. exists (identity (pr1 a)). abstract (exact (eqtohomot (!(functor_id X) (pr1 a)) (pr2 a))). + intros a b c f g. exists (pr1 f · pr1 g). abstract (exact ((pr2 f) @ maponpaths (#X (pr1 f)) (pr2 g) @ (eqtohomot (!(functor_comp X) (pr1 g) (pr1 f)) (pr2 c)))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf.