From 1104780d775bf36ff9f44ab287c22604ab47f0b5 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 10 Apr 2011 03:55:48 +0000 Subject: [PATCH] add natural-iso form of RestrictToImage_splits --- src/Subcategories_ch7_1.v | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 *) -- 1.7.10.4