X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FSubcategories_ch7_1.v;h=e9c89813b14c519c610b1d05e5150beb76459828;hp=cd1eaa9bb6c88d627f7adb25ce71099d07d0bfc2;hb=1104780d775bf36ff9f44ab287c22604ab47f0b5;hpb=658181bed516646957267b055341d9d4b197ed0d

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 *)