fact: Structure Category : Type := {Ob :> Type; Hom : Ob -> Ob -> Setoid; Op_comp : forall a b c : Ob, Map2 (Hom a b) (Hom b c) (Hom a c); Id : forall a : Ob, Hom a a; Prf_ass : Assoc_law Op_comp; Prf_idl : Idl_law Op_comp Id; Prf_idr : Idr_law Op_comp Id}.
imports: Map2