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 BinoidalCategories.
  22 Require Import PreMonoidalCategories.
  23 Require Import PreMonoidalCenter.
  24 Require Import MonoidalCategories_ch7_8.
  25 Require Import Coherence_ch7_8.
  26 Require Import Enrichment_ch2_8.
  27 Require Import RepresentableStructure_ch7_2.
  28 Require Import FunctorCategories_ch7_7.
  29
  30 Require Import NaturalDeduction.
  31 Require Import NaturalDeductionCategory.
  32
  33 Require Import ProgrammingLanguage.
  34 Require Import ProgrammingLanguageGeneralizedArrow.
  35 Require Import FreydCategories.
  36
  37 Require Import GeneralizedArrow.
  38
  39 Section ArrowInLanguage.
  40
  41   (* an Arrow In A Programming Language consists of... *)
  42
  43   (* a host language: *)
  44   Context `(Host:ProgrammingLanguage).
  45
  46   (* ... for which Types(L) is cartesian: *)
  47   Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)).
  48
  49   (* along with a full subcategory of Z(Types(L)) *)
  50   Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P).
  51
  52   Context (Pobj_unit   : P []).
  53   Context (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
  54   Definition VKM :=
  55     PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed.
  56
  57   (* a premonoidal category enriched in aforementioned full subcategory *)
  58   Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK).
  59   Context (KE   :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom).
  60   Context {kbo  :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}.
  61   Context (kbc  :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo).
  62
  63   Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC))
  64   Context (K :@PreMonoidalCat _ _ KE kbo kbc ).
  65   Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))).
  66
  67   Definition ArrowInProgrammingLanguage :=
  68     @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K.
  69
  70   Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
  71     refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.
  72     Defined.
  73
  74 End GArrowInLanguage.