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