From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 9 Apr 2011 02:44:57 +0000 (+0000)
Subject: add RestrictDomain
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=105a7461c7531f8b4e49f34e7242021ac6bb5ebe;hp=758d0e02ca239fb9d9de3810a27290c2d5159294

add RestrictDomain
---

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 :=