formatting fixes

[coq-hetmet.git] / src / GeneralizedArrowFromReification.v

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 627aa22..4a9e790 100644 (file)
--- 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,24 +118,33 @@ 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.
 
-  Lemma garrow_functor_monoidal_niso
-    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> 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.