PreCategory := Eval cbv delta [P_associativity P_left_identity P_right_identity] in @' A Pmor _ Pidentity Pcompose P_associativity P_left_identity P_right_identity.
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.