PreCategory. Proof. refine (@sig' A (fun _ => Unit) (fun s d => @Pmor (pr1_type s) (pr1_type d)) _ (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2) _ _ _); intros; trivial. 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.