X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=627aa223e52c092396bf0652ebe9fcfa3b7e7b50;hp=e6d3cbdb066d13f6da6230195bafcdceada30757;hb=d2526b193694dd7a5c7ab9d80d6b6656a7459bb9;hpb=992203bb4a221ea2f415c0d14bb34d35af2ee637

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index e6d3cbd..627aa22 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -122,9 +122,29 @@ Section GArrowFromReification.
 
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
-  Definition garrow_from_reification : GeneralizedArrow K C.
-    refine {| ga_functor := garrow_functor |}.
+  Lemma garrow_functor_monoidal_niso
+    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+    admit.
+    Defined.
+  Lemma garrow_functor_monoidal_iso
+    : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+    admit.
+    Defined.
+
+  Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
+    { mf_coherence := garrow_functor_monoidal_niso
+    ; mf_id        := garrow_functor_monoidal_iso
+    }.
     admit.
+    admit.
+    admit.
+    Defined.
+
+  Definition garrow_from_reification : GeneralizedArrow K C.
+    refine
+      {| ga_functor          := garrow_functor
+       ; ga_functor_monoidal := garrow_functor_monoidal
+      |}.
     Defined.
 
 End GArrowFromReification.