src/GeneralizedArrowFromReification.v

   1 (*********************************************************************************************************************************)
   2 (* GeneralizedArrowFromReification:                                                                                              *)
   3 (*                                                                                                                               *)
   4 (*   Turn a reification into a generalized arrow                                                                                 *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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.
  28
  29 Section GArrowFromReification.
  30
  31   Context  `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).
  32
  33   Fixpoint garrow_fobj_ vk : C :=
  34     match vk with
  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))
  38     end.
  39
  40   Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)).
  41
  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).
  44     intros.
  45     unfold garrow_fobj.
  46     set (se_decomp _ K  vk) as sevk.
  47     destruct sevk.
  48     simpl in *.
  49     rewrite e.
  50     clear e.
  51     induction x; simpl.
  52
  53     destruct a.
  54       destruct p.
  55
  56       apply iso_inv.
  57         apply (ni_iso (reification_commutes reification e) e0).
  58
  59       eapply id_comp.
  60         apply iso_inv.
  61         apply (mf_id (reification_rstar reification)).
  62         apply (mf_id (me_mf C)).
  63
  64       eapply id_comp.
  65         apply iso_inv.
  66           apply (ni_iso (mf_coherence (reification_rstar reification)) (pair_obj _ _)).
  67         eapply id_comp.
  68           Focus 2.
  69           apply (ni_iso (mf_coherence (me_mf C)) (pair_obj _ _)).
  70           unfold bin_obj.
  71           apply (functors_preserve_isos (enr_v_f C) (a:=(pair_obj _ _))(b:=(pair_obj _ _))).
  72           apply (iso_prod IHx1 IHx2).
  73         Defined.
  74
  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).
  78     Defined.
  79
  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)).
  84     abstract (auto).
  85     Defined.
  86
  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;
  98       apply iso_comp2).
  99     abstract (intros;
 100       unfold step1_mor;
 101       simpl;
 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;
 108       setoid_rewrite qqq;
 109       clear qqq;
 110       setoid_rewrite right_identity;
 111       apply (fmor_preserves_comp reification)).
 112       Defined.
 113
 114   Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))).
 115     exists (fun c1 => homset_tensor_iso c1).
 116     abstract (intros;
 117               simpl;
 118               repeat setoid_rewrite <- associativity;
 119               setoid_rewrite iso_comp1;
 120               setoid_rewrite left_identity;
 121               reflexivity).
 122     Qed.
 123
 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).
 126
 127   (* the generalized arrow is the composition of the two steps *)
 128   Definition garrow_functor := step1_functor >>>> step2_functor.
 129
 130   Lemma garrow_functor_monoidal_iso_i
 131     : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
 132     admit.
 133     Defined.
 134
 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).
 138     admit.
 139     Defined.
 140
 141   Definition garrow_functor_monoidal_niso
 142     : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
 143     admit.
 144     Defined.
 145     Opaque homset_tensor_iso.
 146
 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
 150     }.
 151     admit.
 152     admit.
 153     admit.
 154     Defined.
 155
 156   Definition garrow_from_reification : GeneralizedArrow K C.
 157     refine
 158       {| ga_functor          := garrow_functor
 159        ; ga_functor_monoidal := garrow_functor_monoidal
 160       |}.
 161     Defined.
 162
 163 End GArrowFromReification.
 164 Opaque homset_tensor_iso.