(*********************************************************************************************************************************)
(* GeneralizedArrowFromReification: *)
(* *)
-(* Turn a generalized arrow into a reification *)
+(* Turn a reification into a generalized arrow *)
(* *)
(*********************************************************************************************************************************)
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;
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;
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.