PreCategory. refine (@Build_PreCategory (forall a : A, P a) (fun s d => forall a : A, morphism (P a) (s a) (d a)) (fun x => fun a => identity (x a)) (fun s d d' m2 m1 => fun a => m2 a o m1 a) _ _ _ _); abstract ( repeat (intro || apply path_forall); auto with morphism ). Defined.
Require Import Category.Strict. Require Import Basics.Trunc.