+ Definition ff_functor_section_splits_niso_helper' a
+ : ((RestrictToImage F >>>> ff_functor_section_functor) a ≅ (functor_id _) a).
+ intros; simpl.
+ unfold functor_fobj.
+ unfold ff_functor_section_fobj.
+ unfold RestrictToImage_fobj.
+ simpl.
+ apply iso_id.
+ Defined.
+
+ Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
+ intros; simpl.
+ exists ff_functor_section_splits_niso_helper'.
+ intros.
+ simpl in *.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ set (F_full _ _ (F \ f)) as qr.
+ destruct qr.
+ apply F_faithful in e.
+ symmetry.
+ auto.
+ Qed.
+
+ Context (CF:ConservativeFunctor F).
+
+ Lemma if_fullimage `{C0:Category}{Aobj}{Bobj}{A:Functor C0 C1 Aobj}{B:Functor C0 C1 Bobj} :
+ A >>>> F ≃ B >>>> F ->
+ A >>>> RestrictToImage F ≃ B >>>> RestrictToImage F.
+ intro H.
+ destruct H.
+ unfold IsomorphicFunctors.
+ set (fun A => functors_preserve_isos (RestrictToImage F) (cf_reflect_iso _ _ (x A))).
+ exists i.
+ intros.
+ unfold RestrictToImage.
+ unfold functor_comp.
+ simpl.
+ unfold functor_comp in H.
+ simpl in H.
+ rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x A0)).
+ rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x B0)).
+ apply H.
+ Qed.
+