From 105a7461c7531f8b4e49f34e7242021ac6bb5ebe Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 9 Apr 2011 02:44:57 +0000 Subject: [PATCH] add RestrictDomain --- src/Subcategories_ch7_1.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v index a06e07e..cd1eaa9 100644 --- a/src/Subcategories_ch7_1.v +++ b/src/Subcategories_ch7_1.v @@ -122,6 +122,25 @@ Section FullImage. End FullImage. +(* any functor may be restricted to a subcategory of its domain *) +Section RestrictDomain. + + Context `{C:Category}. + Context `{D:Category}. + Context `(F:!Functor C D fobj). + Context {Pmor}(S:WideSubcategory C Pmor). + + Instance RestrictDomain : Functor S D fobj := + { fmor := fun a b f => F \ (projT1 f) }. + intros; destruct f; destruct f'; simpl in *. + apply fmor_respects; auto. + intros. simpl. apply fmor_preserves_id. + intros; simpl; destruct f; destruct g; simpl in *. + apply fmor_preserves_comp. + Defined. + +End RestrictDomain. + (* Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor) {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj := -- 1.7.10.4