X `{IsTrunc 1 X} : PreCategory. Proof. refine (@Build_PreCategory X (@paths X) (@GroupoidCategoryInternals.identity X) (@GroupoidCategoryInternals.compose X) _ _ _ _); simpl; intros; path_induction; reflexivity. Defined.
Require Import Category.Morphisms Category.Strict. Require Import Trunc PathGroupoids Basics.Tactics.