X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=f17caa5c4d2c22a6696134ab31973b3d6d6ae2b7;hp=e6d3cbdb066d13f6da6230195bafcdceada30757;hb=e536cc4194f350ed6de5d465bcf53fda650b3d12;hpb=3351499d7cb3d32c8df441426309ec6a1ef2a035;ds=sidebyside

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index e6d3cbd..f17caa5 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -107,6 +107,14 @@ Section GArrowFromReification.
       apply (fmor_preserves_comp reification)).
       Defined.
 
+(*
+  Definition FullImage_Monoidal 
+    `(F:@Functor Cobj CHom C1 Dobj DHom D1 Fobj) `(mc:MonoidalCat D1 Mobj MF) : MonoidalCat (FullImage F) Mobj.
+
+  Definition step1_functor_monoidal : MonoidalFunctor (enr_v_mon K) step1_functor.
+    admit.
+    Defined.
+*)
   Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))).
     exists (fun c1 => homset_tensor_iso c1).
     abstract (intros;
@@ -124,6 +132,11 @@ Section GArrowFromReification.
 
   Definition garrow_from_reification : GeneralizedArrow K C.
     refine {| ga_functor := garrow_functor |}.
+    (*
+    unfold garrow_functor.
+    apply MonoidalFunctorsCompose.
+    apply MonoidalFunctorsCompose.
+    *)
     admit.
     Defined.