Definition make_is_precategory_one_assoc {C : precategory_data} (H1 : ∏ (a b : C) (f : a --> b), identity a · f = f) (H2 : ∏ (a b : C) (f : a --> b), f · identity b = f) (H3 : ∏ (a b c d : C) (f : a --> b) (g : b --> c) (h : c --> d), f · (g · h) = (f · g) · h) : is_precategory C := (H1,,H2),,(H3,,λ a b c d f g h, pathsinv0 (H3 a b c d f g h)).
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.