From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sun, 10 Apr 2011 03:55:48 +0000 (+0000)
Subject: add natural-iso form of RestrictToImage_splits
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=1104780d775bf36ff9f44ab287c22604ab47f0b5;ds=inline

add natural-iso form of RestrictToImage_splits
---

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index cd1eaa9..e9c8981 100644
--- 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 *)