1 (*********************************************************************************************************************************)
2 (* GeneralizedArrowFromReification: *)
4 (* Turn a reification into a generalized arrow *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import Functors_ch1_4.
13 Require Import Isomorphisms_ch1_5.
14 Require Import ProductCategories_ch1_6_1.
15 Require Import OppositeCategories_ch1_6_2.
16 Require Import Enrichment_ch2_8.
17 Require Import Subcategories_ch7_1.
18 Require Import NaturalTransformations_ch7_4.
19 Require Import NaturalIsomorphisms_ch7_5.
20 Require Import BinoidalCategories.
21 Require Import PreMonoidalCategories.
22 Require Import MonoidalCategories_ch7_8.
23 Require Import Coherence_ch7_8.
24 Require Import Enrichment_ch2_8.
25 Require Import RepresentableStructure_ch7_2.
26 Require Import Reification.
27 Require Import GeneralizedArrow.
29 Section GArrowFromReification.
31 Context `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).
33 Fixpoint garrow_fobj_ vk : C :=
35 | T_Leaf None => me_i C
36 | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end
37 | t1,,t2 => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2))
40 Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)).
42 Definition homset_tensor_iso
43 : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk).
46 set (se_decomp _ K vk) as sevk.
57 apply (ni_iso (reification_commutes reification e) e0).
61 apply (mf_id (reification_rstar reification)).
62 apply (mf_id (me_mf C)).
66 apply (ni_iso (mf_coherence (reification_rstar reification)) (pair_obj _ _)).
69 apply (ni_iso (mf_coherence (me_mf C)) (pair_obj _ _)).
71 apply (functors_preserve_isos (enr_v_f C) (a:=(pair_obj _ _))(b:=(pair_obj _ _))).
72 apply (iso_prod IHx1 IHx2).
75 Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (HomFunctor C (me_i C)).
76 exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)).
77 abstract (exists (garrow_fobj vk); auto).
80 Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (HomFunctor C (me_i C))}~~>(garrow_fobj' b).
81 exists (iso_backward (homset_tensor_iso a)
82 >>> reification_rstar reification \ f
83 >>> iso_forward (homset_tensor_iso b)).
87 (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor
88 * to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
89 Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'.
90 refine {| fmor := fun a b f => step1_mor f |}.
91 abstract (intros; unfold step1_mor; simpl;
92 apply comp_respects; try reflexivity;
93 apply comp_respects; try reflexivity;
94 apply fmor_respects; auto).
95 abstract (intros; unfold step1_mor; simpl;
96 setoid_rewrite fmor_preserves_id;
97 setoid_rewrite right_identity;
102 repeat setoid_rewrite <- associativity;
103 apply comp_respects; try reflexivity;
104 repeat setoid_rewrite associativity;
105 apply comp_respects; try reflexivity;
106 setoid_rewrite juggle2;
107 set (iso_comp1 (homset_tensor_iso b)) as qqq;
110 setoid_rewrite right_identity;
111 apply (fmor_preserves_comp reification)).
114 Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))).
115 exists (fun c1 => homset_tensor_iso c1).
118 repeat setoid_rewrite <- associativity;
119 setoid_rewrite iso_comp1;
120 setoid_rewrite left_identity;
124 (* the "step2_functor" is the section of the Hom(I,-) functor *)
125 Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C).
127 (* the generalized arrow is the composition of the two steps *)
128 Definition garrow_functor := step1_functor >>>> step2_functor.
130 Lemma garrow_functor_monoidal_iso_i
131 : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
135 Lemma garrow_functor_monoidal_iso :
136 forall X Y:enr_v_mon K,
137 garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y).
141 Definition garrow_functor_monoidal_niso
142 : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
145 Opaque homset_tensor_iso.
147 Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
148 { mf_coherence := garrow_functor_monoidal_niso
149 ; mf_id := garrow_functor_monoidal_iso_i
156 Definition garrow_from_reification : GeneralizedArrow K C.
158 {| ga_functor := garrow_functor
159 ; ga_functor_monoidal := garrow_functor_monoidal
163 End GArrowFromReification.
164 Opaque homset_tensor_iso.