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 (*
 121 Section ArrowInLanguage.
 122
 123   (* an Arrow In A Programming Language consists of... *)
 124
 125   (* a host language: *)
 126   Context `(Host:ProgrammingLanguage).
 127
 128   (* ... for which Types(L) is cartesian: *)
 129   Context {MF}(center_of_TypesL:MonoidalCat (TypesL _ _ Host) (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []).
 130
 131   (* along with a monoidal subcategory of Z(Types(L)) *)
 132   Context (VK:MonoidalSubCat center_of_TypesL).
 133
 134   (* a premonoidal category enriched in aforementioned full subcategory *)
 135   Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK).
 136 Check (@ECategory).
 137   Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom).
 138
 139 Check (Underlying KE).
 140
 141   Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}.
 142
 143   Context (kbc:@BinoidalCat center_of_TypesL _ (Underlying KE) kbo).
 144
 145   Check (@PreMonoidalCat)
 146   Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC))
 147   Context (K:@PreMonoidalCat _ _ KE kbo kbc ).
 148   Context (CC:CartesianCat center_of_TypesL).
 149
 150   (*
 151   Definition K_enrichment : Enrichment.
 152     refine {| enr_c := KE |}.
 153     Defined.
 154   Context (K_surjective:SurjectiveEnrichment K_enrichment).
 155     *)
 156 Check (@FreydCategory).
 157
 158   Definition ArrowInProgrammingLanguage :=
 159     @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.
 160
 161   Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
 162     refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.
 163     Defined.
 164
 165 End GArrowInLanguage.
 166 *)