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:
658181b
)
add natural-iso form of RestrictToImage_splits
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 10 Apr 2011 03:55:48 +0000
(
03:55
+0000)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 10 Apr 2011 03:55:48 +0000
(
03:55
+0000)
src/Subcategories_ch7_1.v
patch
|
blob
|
history
diff --git
a/src/Subcategories_ch7_1.v
b/src/Subcategories_ch7_1.v
index
cd1eaa9
..
e9c8981
100644
(file)
--- a/
src/Subcategories_ch7_1.v
+++ b/
src/Subcategories_ch7_1.v
@@
-120,6
+120,16
@@
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 *)