+ Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
+ intro H.
+ unfold WeaklyMonic; intros.
+ apply (if_comp(F2:=G>>>>functor_id _)).
+ apply if_inv.
+ apply if_right_identity.
+ apply if_inv.
+ apply (if_comp(F2:=H0>>>>functor_id _)).
+ apply if_inv.
+ apply if_right_identity.
+ eapply if_inv.
+ apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
+ apply (if_respects G G (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)).
+ apply if_id.
+ apply if_inv.
+ apply ff_functor_section_splits_niso'.
+ apply if_inv.
+ apply (if_comp(F2:=H0>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
+ apply (if_respects H0 H0 (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)).
+ apply if_id.
+ apply if_inv.
+ apply ff_functor_section_splits_niso'.
+ assert
+ ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
+ ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
+ apply if_inv.
+ apply (if_associativity H0 (RestrictToImage F) ff_functor_section_functor).
+ apply (if_comp H2).
+ clear H2.
+ apply if_inv.
+ assert
+ ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
+ ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
+ apply if_inv.
+ apply (if_associativity G (RestrictToImage F) ff_functor_section_functor).
+ apply (if_comp H2).
+ clear H2.
+ apply (if_respects (G >>>> RestrictToImage F) (H0 >>>> RestrictToImage F)
+ ff_functor_section_functor ff_functor_section_functor).
+ apply if_fullimage.
+ apply H1.
+ simpl.
+ exists (ni_id _).
+ intros.
+ simpl.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ reflexivity.
+ Qed.