projects
/
coq-categories.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f494aec
)
add FullSubcategoryInclusionFunctor
author
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 11 Apr 2011 03:15:21 +0000
(
03:15
+0000)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Mon, 11 Apr 2011 03:15:21 +0000
(
03:15
+0000)
src/Subcategories_ch7_1.v
patch
|
blob
|
history
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 :=