PreCategory := Eval cbv delta [P_associativity P_left_identity P_right_identity] in @' A Pobj Pmor _ Pidentity Pcompose P_associativity P_left_identity P_right_identity.
Require Import Category.Core Functor.Core. Require Import Basics.Trunc Types.Sigma.