Definition make_precategory_one_assoc (C : precategory_data) (H : is_precategory_one_assoc C) : precategory := tpair _ C (is_precategory_one_assoc_to_two C H).
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.