From 20641452e40570b4bfc9429ca57b0cffca6eccfb Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 03:15:21 +0000 Subject: [PATCH] add FullSubcategoryInclusionFunctor --- src/Subcategories_ch7_1.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v index e9c8981..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 := -- 1.7.10.4