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
| 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.
Definition garrow_functor := step1_functor >>>> step2_functor.
- Definition garrow_from_reification : GeneralizedArrow K C.
- refine {| ga_functor := garrow_functor |}.
+ 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.