Definition total_morphisms (C : precategory_ob_mor) := total2 ( fun ab : dirprod (ob C)(ob C) => precategory_morphisms (pr1 ab) (pr2 ab)).
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories.