Definition makecategory_data (obj : UU) (mor : obj -> obj -> UU) (identity : ∏ i, mor i i) (compose : ∏ i j k (f:mor i j) (g:mor j k), mor i k) : precategory_data := make_precategory_data (makecategory_ob_mor obj mor) identity compose.
Require Import UniMath.MoreFoundations.Tactics.