fact: Record PreCategory := Build_PreCategory' { object :> Type; morphism : object -> object -> Type; identity : forall x, morphism x x; compose : forall s d d', morphism d d' -> morphism s d -> morphism s d' where "f 'o' g" := (compose f g); associativity : forall x1 x2 x3 x4 (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4), (m3 o m2) o m1 = m3 o (m2 o m1); associativity_sym : forall x1 x2 x3 x4 (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4), m3 o (m2 o m1) = (m3 o m2) o m1; left_identity : forall a b (f : morphism a b), identity b o f = f; right_identity : forall a b (f : morphism a b), f o identity a = f; identity_identity : forall x, identity x o identity x = identity x; trunc_morphism : forall s d, IsHSet (morphism s d) }.
imports: Overture Basics.Notations