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

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index e6d3cbd..4a9e790 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -1,7 +1,7 @@
 (*********************************************************************************************************************************)
 (* GeneralizedArrowFromReification:                                                                                              *)
 (*                                                                                                                               *)
-(*   Turn a generalized arrow into a reification                                                                                 *)
+(*   Turn a reification into a generalized arrow                                                                                 *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
@@ -70,19 +70,21 @@ Section GArrowFromReification.
           apply (iso_prod IHx1 IHx2).
         Defined.
 
-  Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (RepresentableFunctor C (me_i C)).
+  Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (HomFunctor C (me_i C)).
     exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)).
     abstract (exists (garrow_fobj vk); auto).
     Defined.
 
-  Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (RepresentableFunctor C (me_i C))}~~>(garrow_fobj' b).
+  Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (HomFunctor C (me_i C))}~~>(garrow_fobj' b).
     exists (iso_backward (homset_tensor_iso a) 
         >>> reification_rstar reification \ f
         >>> iso_forward (homset_tensor_iso  b)).
     abstract (auto).
     Defined.
 
-  Definition step1_functor : Functor (enr_v_mon K) (FullImage (RepresentableFunctor C (me_i C))) garrow_fobj'.
+  (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor
+   * to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
+  Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'.
     refine {| fmor := fun a b f => step1_mor f |}.
     abstract (intros; unfold step1_mor; simpl;
               apply comp_respects; try reflexivity;
@@ -107,7 +109,7 @@ Section GArrowFromReification.
       apply (fmor_preserves_comp reification)).
       Defined.
 
-  Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))).
+  Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))).
     exists (fun c1 => homset_tensor_iso c1).
     abstract (intros;
               simpl;
@@ -116,16 +118,45 @@ 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).
 
+  (* the generalized arrow is the composition of the two steps *)
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
-  Definition garrow_from_reification : GeneralizedArrow K C.
-    refine {| ga_functor := 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 :
+    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_i
+    }.
+    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.
 Opaque homset_tensor_iso.