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