X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FSubcategories_ch7_1.v;h=25391a12eda6a431ed4bac1e99f4d432314bc903;hp=a06e07e4fbe06591b4a9fd1bad37537c51920ae4;hb=0ecd73c172f67634fa956fb52b332e6effb5a04d;hpb=c722b7a165e09570b767e3314d0b0329fc19962e

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index a06e07e..25391a1 100644
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -44,16 +44,15 @@ Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True
   intros; auto.
   intros; auto.
   Defined.
+*)
 (* the inclusion operation from a subcategory to its host is a functor *)
-Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
+Instance FullSubcategoryInclusionFunctor `(SP:@FullSubcategory Ob Hom C Pobj)
   : Functor SP C (fun x => projT1 x) :=
-  { fmor := fun dom ran f => projT1 f }.
+  { fmor := fun dom ran f => f }.
   intros. unfold eqv in H. simpl in H. auto.
   intros. simpl. reflexivity.
   intros. simpl. reflexivity.
   Defined.
-*)
-
 
 (* 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 :=
@@ -120,8 +119,37 @@ Section FullImage.
     auto.
     Defined.
 
+  Lemma RestrictToImage_splits_niso : F ≃ (RestrictToImage >>>> FullImage_InclusionFunctor).
+    unfold IsomorphicFunctors.
+    exists (fun A => iso_id (fobj A)).
+    intros.
+    simpl.
+    setoid_rewrite left_identity.
+    setoid_rewrite right_identity.
+    reflexivity.
+    Qed.
+
 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 :=