src/ProgrammingLanguageArrow.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguageArrow                                                                                                      *)
   3 (*                                                                                                                               *)
   4 (*   Arrows in ProgrammingLanguages.                                                                                             *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import InitialTerminal_ch2_2.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import FunctorCategories_ch7_7.
  26
  27 Require Import NaturalDeduction.
  28 Require Import NaturalDeductionCategory.
  29
  30 Require Import ProgrammingLanguage.
  31 Require Import ProgrammingLanguageGeneralizedArrow.
  32 Require Import FreydCategories.
  33
  34 Require Import GeneralizedArrow.
  35
  36 Section ExtendFunctor.
  37
  38   Context `(F:Functor).
  39   Context  (P:c1 -> Prop).
  40
  41   Definition domain_subcat := FullSubcategory c1 P.
  42
  43   Definition functor_restricts_to_full_subcat_on_domain_fobj (a:domain_subcat) : c2 :=
  44     F (projT1 a).
  45
  46   Definition functor_restricts_to_full_subcat_on_domain_fmor (a b:domain_subcat)(f:a~~{domain_subcat}~~>b) :
  47     (functor_restricts_to_full_subcat_on_domain_fobj a)~~{c2}~~>(functor_restricts_to_full_subcat_on_domain_fobj b) :=
  48     F \ (projT1 f).
  49
  50   Lemma functor_restricts_to_full_subcat_on_domain : Functor domain_subcat c2 functor_restricts_to_full_subcat_on_domain_fobj.
  51     refine {| fmor := functor_restricts_to_full_subcat_on_domain_fmor |};
  52       unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros.
  53     setoid_rewrite H; reflexivity.
  54     setoid_rewrite fmor_preserves_id; reflexivity.
  55     setoid_rewrite <- fmor_preserves_comp; reflexivity.
  56     Defined.
  57
  58 End ExtendFunctor.
  59
  60 Section MonoidalSubCat.
  61
  62   (* a monoidal subcategory is a full subcategory, closed under tensor and containing the unit object *)
  63   Class MonoidalSubCat {Ob}{Hom}{C:Category Ob Hom}{MFobj}{MF}{MI}(MC:MonoidalCat C MFobj MF MI) :=
  64   { msc_P                   :  MC -> Prop
  65   ; msc_closed_under_tensor :  forall o1 o2, msc_P o1 -> msc_P o2 -> msc_P (MC (pair_obj o1 o2))
  66   ; msc_contains_unit       :  msc_P (mon_i MC)
  67   ; msc_subcat              := FullSubcategory MC msc_P
  68   }.
  69   Local Coercion msc_subcat : MonoidalSubCat >-> SubCategory.
  70
  71   Context `(MSC:MonoidalSubCat).
  72
  73   (* any full subcategory of a monoidal category, , is itself monoidal *)
  74   Definition mf_restricts_to_full_subcat_on_domain_fobj (a:MSC ×× MSC) : MSC.
  75     destruct a.
  76     destruct o.
  77     destruct o0.
  78     set (MC (pair_obj x x0)) as m'.
  79     exists m'.
  80     apply msc_closed_under_tensor; auto.
  81     Defined.
  82
  83   Definition mf_restricts_to_full_subcat_on_domain_fmor
  84     {a}{b}
  85     (f:a~~{MSC ×× MSC}~~>b)
  86     :
  87     (mf_restricts_to_full_subcat_on_domain_fobj a)~~{MSC}~~>(mf_restricts_to_full_subcat_on_domain_fobj b).
  88     destruct a as [[a1 a1pf] [a2 a2pf]].
  89     destruct b as [[b1 b1pf] [b2 b2pf]].
  90     destruct f as [[f1 f1pf] [f2 f2pf]].
  91     simpl in *.
  92     exists (MC \ (pair_mor (pair_obj a1 a2) (pair_obj b1 b2) f1 f2)); auto.
  93     Defined.
  94
  95   Lemma mf_restricts_to_full_subcat_on_domain : Functor (MSC ×× MSC) MSC
  96     mf_restricts_to_full_subcat_on_domain_fobj.
  97     refine {| fmor := fun a b f => mf_restricts_to_full_subcat_on_domain_fmor f |};
  98       unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros.
  99     admit.
 100     admit.
 101     admit.
 102     Defined.
 103
 104   Definition subcat_i : MSC.
 105     exists (mon_i MC).
 106     apply msc_contains_unit.
 107     Defined.
 108
 109   Lemma full_subcat_is_monoidal : MonoidalCat MSC _ mf_restricts_to_full_subcat_on_domain subcat_i.
 110     admit.
 111     Defined.
 112
 113   Lemma inclusion_functor_monoidal : MonoidalFunctor full_subcat_is_monoidal MC (InclusionFunctor _ MSC).
 114     admit.
 115     Defined.
 116
 117 End MonoidalSubCat.
 118 Coercion full_subcat_is_monoidal : MonoidalSubCat >-> MonoidalCat.
 119
 120 Section ArrowInLanguage.
 121
 122   (* an Arrow In A Programming Language consists of... *)
 123
 124   (* a host language: *)
 125   Context (Host:ProgrammingLanguageSMME).
 126
 127   (* ... for which Types(L) is cartesian: *)
 128   Context {MF}(center_of_TypesL:MonoidalCat (TypesL _ _ Host) (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []).
 129
 130   (* along with a monoidal subcategory of Z(Types(L)) *)
 131   Context (VK:MonoidalSubCat center_of_TypesL).
 132
 133   (* a premonoidal category enriched in aforementioned full subcategory *)
 134   Context {Kehom:center_of_TypesL -> center_of_TypesL -> VK}.
 135
 136   Context {KE:@ECategory _ _ VK _ _ _ VK center_of_TypesL Kehom}.
 137
 138   Context (CC:CartesianCat center_of_TypesL).
 139
 140   Context {kbo}{kbc}(K:@PreMonoidalCat _ _ KE kbo kbc (@one _ _ _ (car_terminal(CartesianCat:=CC)))).
 141
 142   (*
 143   Definition K_enrichment : Enrichment.
 144     refine {| enr_c := KE |}.
 145     Defined.
 146   Context (K_surjective:SurjectiveEnrichment K_enrichment).
 147     *)
 148
 149   Definition ArrowInProgrammingLanguage :=
 150     @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.
 151
 152   Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
 153     refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.
 154     Defined.
 155
 156 End GArrowInLanguage.