(X : Type) : PreCategory. Proof. refine (@Build_PreCategory X _ (@FundamentalPreGroupoidCategoryInternals.identity X) (@FundamentalPreGroupoidCategoryInternals.compose X) _ _ _ _); simpl; intros; abstract ( repeat match goal with | [ m : Trunc _ _ |- _ ] => revert m; apply Trunc_ind; [ intro; match goal with | [ |- IsHSet (?a = ?b :> ?T) ] => generalize a b; intros; let H := fresh in assert (H : forall x y : T, IsHProp (x = y)) end; typeclasses eauto | intro ] end; simpl; apply ap; first [ apply concat_p_pp | apply concat_1p | apply concat_p1 ] ). Defined.
Require Import Category.Core. Require Import HoTT.Truncations.Core. Require Import HoTT.Basics.