theory.hom_functor

Require Import
  Relation_Definitions
  abstract_algebra theory.setoids interfaces.functors theory.categories.

Require categories.setoids.

Section contents.

  Context `{Category C} (x: C).

  Definition homFrom (y: C): setoids.Object := @setoids.object (x y) _ _.

  Global Program Instance: Fmap homFrom := λ v w X, (X ◎): (x v) (x w).

  Global Instance: Functor homFrom _.

End contents.