PreCategory := @Build_PreCategory (sig_type Pobj) (fun s d => morphism A (pr1_type s) (pr1_type d)) (fun x => @identity A (pr1_type x)) (fun s d d' m1 m2 => m1 o m2)%morphism (fun _ _ _ _ => associativity A _ _ _ _) (fun _ _ => left_identity A _ _) (fun _ _ => right_identity A _ _) _.
Require Import HoTT.Basics HoTT.Types. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.