X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FGeneralizedArrowFromReification.v;h=15d1b091e34401be7beebf90bd8fb276677657aa;hb=d1a4d10de986d774d3cfb10348036cb60bc80277;hp=356ee579c605703ab589a6ae6692b2ee3b06bcf3;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;p=coq-hetmet.git

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 356ee57..15d1b09 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -17,6 +17,8 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
@@ -118,7 +120,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 +127,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.