(* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *)
Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type :=
(* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *)
Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type :=