-(* any functor may be restricted to its image *)
-Section RestrictToImage.
- Context `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)).
- Definition RestrictToImage_fobj : C -> FullImage F.
- intros.
- exists (F X).
- exists X.
- reflexivity.
- Defined.
- Definition RestrictToImage_fmor a b (f:a~>b) : (RestrictToImage_fobj a)~~{FullImage F}~~>(RestrictToImage_fobj b).
- exists (F \ f); auto.
+ Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) :=
+ { id := fun t => id (F t)
+ ; eqv := fun x y f g => eqv(Category:=D) _ _ f g
+ ; comp := fun x y z f g => comp(Category:=D) _ _ _ f g
+ }.
+ intros; apply Build_Equivalence. unfold Reflexive.
+ intros; reflexivity.
+ unfold Symmetric; intros; simpl; symmetry; auto.
+ unfold Transitive; intros; simpl. transitivity y; auto.
+ intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
+ intros; simpl. apply left_identity.
+ intros; simpl. apply right_identity.
+ intros; simpl. apply associativity.
+ Defined.
+
+ Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) :=
+ { fmor := fun x y f => f }.
+ intros; auto.
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.