Definition makecategory (obj : UU) (mor : obj -> obj -> UU) (homsets : ∏ a b, isaset (mor a b)) (identity : ∏ i, mor i i) (compose : ∏ i j k (f:mor i j) (g:mor j k), mor i k) (right : ∏ i j (f:mor i j), compose _ _ _ (identity i) f = f) (left : ∏ i j (f:mor i j), compose _ _ _ f (identity j) = f) (associativity : ∏ a b c d (f:mor a b) (g:mor b c) (h:mor c d), compose _ _ _ f (compose _ _ _ g h) = compose _ _ _ (compose _ _ _ f g) h) (associativity' : ∏ a b c d (f:mor a b) (g:mor b c) (h:mor c d), compose _ _ _ (compose _ _ _ f g) h = compose _ _ _ f (compose _ _ _ g h)) : category := (make_precategory (make_precategory_data (make_precategory_ob_mor obj (λ i j, mor i j)) identity compose) ((right,,left),,(associativity,,associativity'))),,homsets.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.