Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import MonoidalCategories_ch7_8.
Section RepresentableStructure.
Context `(ec:ECategory(mn:=mn)(V:=V)).
apply hom_covariant_distributes.
Defined.
+ (*
Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
simpl.
setoid_rewrite <- associativity.
set (@eqv_equivalence) as qmt.
apply qmt.
Qed.
-
+ *)
End RepresentableStructure.
Opaque HomFunctor.