X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FSubcategories_ch7_1.v;h=78bf98fe8e649620bf633c49f6639e0c7bd93ebd;hp=e6b8aa4361d776657419b2a9f8317b468ebedddb;hb=27ffdd2265eb1c15acc62970f49d25a07bcadb05;hpb=b0262af94b62376527556d79b10c4f1de29a9565

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index e6b8aa4..78bf98f 100644
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -94,7 +94,7 @@ Section RestrictToImage.
     Qed.
 End RestrictToImage.
 
-Instance func_opSubcat `(c1:Category Ob1 Hom1)`(c2:Category Ob Hom)`(SP:@SubCategory _ _ c2 Pobj Pmor)
+Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
   {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
   { fmor                := fun a b f => fmor F f }.
   intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
@@ -190,7 +190,7 @@ Definition WeaklyMonic
     `{D:Category}
      {Fobj}
      (F:@Functor _ _ C _ _ D Fobj) := forall
-    `{E:Category}
+     Eob EHom (E:@Category Eob EHom)
     `{G :@Functor _ _ E _ _ C Gobj'}
     `{H :@Functor _ _ E _ _ C Hobj'},
     G >>>> F ≃ H >>>> F