X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=4a9e7908ce49a83d2626bf3a7daba72cf9d0a271;hp=356ee579c605703ab589a6ae6692b2ee3b06bcf3;hb=6ef9f270b138fc7aab48013d55a8192ff022c0f1;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 356ee57..4a9e790 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -118,7 +118,6 @@ Section GArrowFromReification.
               setoid_rewrite left_identity;
               reflexivity).
     Qed.
-    Opaque homset_tensor_iso.
 
   (* the "step2_functor" is the section of the Hom(I,-) functor *)
   Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C).
@@ -126,19 +125,26 @@ Section GArrowFromReification.
   (* the generalized arrow is the composition of the two steps *)
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
-  Lemma garrow_functor_monoidal_niso
-    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
-    unfold garrow_functor.
+  Lemma garrow_functor_monoidal_iso_i
+    : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
     admit.
     Defined.
-  Lemma garrow_functor_monoidal_iso
-    : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+
+  Lemma garrow_functor_monoidal_iso :
+    forall X Y:enr_v_mon K, 
+      garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y).
     admit.
     Defined.
 
+  Definition garrow_functor_monoidal_niso
+    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+    admit.
+    Defined.
+    Opaque homset_tensor_iso.
+
   Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
-    { mf_coherence := garrow_functor_monoidal_niso
-    ; mf_id        := garrow_functor_monoidal_iso
+    { mf_coherence   := garrow_functor_monoidal_niso
+    ; mf_id          := garrow_functor_monoidal_iso_i
     }.
     admit.
     admit.