Definition total_precategory_ob_mor_of_set_functor {C : setcategory} (F : C ⟶ cat_of_setcategory) : precategory_ob_mor. Proof. use make_precategory_ob_mor. - exact (∑ (x : ob C), ob (pr1 (F x))). - exact (λ x y, ∑ (f : pr1 x --> pr1 y), pr1 (#F f) (pr2 x) --> pr2 y). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories.