PreCategory. Proof. refine (@Build_PreCategory Pair (fun s d => morphism s d) identity compose _ _ _ _); abstract ( repeat intro; apply path_sigma_uncurried; simpl; ((exists (associativity _ _ _ _ _ _ _ _)) || (exists (left_identity _ _ _ _)) || (exists (right_identity _ _ _ _))); exact (center _) ). Defined.
Require Import Category.Core Functor.Core. Require Import SetCategory.Core. Require Import Basics.Trunc Types.Sigma. Require Import Basics.Tactics.