Definition make_precategory_ob_mor (ob : UU)(mor : ob -> ob -> UU) : precategory_ob_mor := tpair _ ob mor.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.