checkpoint

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

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 6aeaace..f17caa5 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -26,7 +26,7 @@ Require Import GeneralizedArrow.
 
 Section GArrowFromReification.
 
-  Context  (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)).
+  Context  `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).
 
   Fixpoint garrow_fobj_ vk : C :=
     match vk with
@@ -35,13 +35,13 @@ Section GArrowFromReification.
     | t1,,t2          => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
     end.
 
-  Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp K vk)).
+  Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)).
 
   Definition homset_tensor_iso
     : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk).
     intros.
     unfold garrow_fobj.
-    set (se_decomp K vk) as sevk.
+    set (se_decomp _ K  vk) as sevk.
     destruct sevk.
     simpl in *.
     rewrite e.
@@ -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.