- Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
- Definition RepresentableFunctor (X:ec) : Functor ec V (fun a => X~~>a) :=
- func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor.
-
- Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f).
+ Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
+ *)
+
+ Definition HomFunctor (X:ec) : Functor ec V (ehom X).
+ refine {| fmor := @hom_covariant X |}.
+ intros.
+ unfold hom_covariant.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ apply fmor_respects; auto.
+ intros.
+ unfold hom_covariant.
+ apply (epic _ (iso_epic ((pmon_cancelr) (X ~~> a)))).
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ setoid_rewrite iso_comp1.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ apply (@eright_identity).
+ intros.
+ symmetry.
+ apply hom_covariant_distributes.
+ Defined.
+
+ (*
+ Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).