almost finished with main theorem

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

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index f17caa5..627aa22 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -107,14 +107,6 @@ 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;
@@ -130,15 +122,30 @@ Section GArrowFromReification.
 
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
-  Definition garrow_from_reification : GeneralizedArrow K C.
-    refine {| ga_functor := garrow_functor |}.
-    (*
-    unfold garrow_functor.
-    apply MonoidalFunctorsCompose.
-    apply MonoidalFunctorsCompose.
-    *)
+  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.
 Opaque homset_tensor_iso.