Definition cat_of_elems_ob_mor : precategory_ob_mor. Proof. exists (∑ (c : C), X c : hSet). intros a b. apply (∑ (f : C⟦pr1 a,pr1 b⟧), (pr2 a) = # X f (pr2 b)). 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.