add FullSubcategoryInclusionFunctor

[coq-categories.git] / src / Subcategories_ch7_1.v

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index cd1eaa9..25391a1 100644 (file)
--- 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.
   intros; auto.
   intros; auto.
   Defined.

+*)

 (* the inclusion operation from a subcategory to its host is a functor *)
 (* 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) :=
   : 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.
   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 :=
 
 (* 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,6 +119,16 @@ Section FullImage.
     auto.
     Defined.
 
     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 *)
 End FullImage.
 
 (* any functor may be restricted to a subcategory of its domain *)