sig_mor' : PreCategory. Proof. refine (@Build_PreCategory (object A) (fun s d => mor s d) (fun x => identity x) (fun s d d' m1 m2 => compose m1 m2) _ _ _ _); assumption. Defined.
Require Import HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.