add natural-iso form of RestrictToImage_splits

[coq-categories.git] / src / Subcategories_ch7_1.v

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