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 FreydCategories.
  35 Require Import Enrichments.
  36 Require Import GeneralizedArrow.
  37
  38 Section ArrowInLanguage.
  39
  40   (* an Arrow In A Programming Language consists of... *)
  41
  42   (* a host language: *)
  43   Context `(Host         : ProgrammingLanguage).
  44
  45   Context  (Host_Monoidal  : MonoidalCat  (TypesL_PreMonoidal Host)).
  46   Context  (Host_Cartesian : CartesianCat Host_Monoidal).
  47
  48   Context
  49     {P}
  50     (Pobj_unit   : P [])
  51     (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
  52
  53   Context (VK : FullSubcategory Host_Cartesian P).
  54
  55   Context  ehom KE (K_bin:@EBinoidalCat _ _ VK _ _ _
  56           (PreMonoidalFullSubcategory_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed)
  57           (TypesL Host) ehom KE (bin_obj(BinoidalCat:=Host_Monoidal))).
  58
  59   Context (K_premonoidal:PreMonoidalCat K_bin (one(TerminalObject:=Host_Cartesian))).
  60
  61   Definition ArrowInProgrammingLanguage :=
  62     @FreydCategory _ _ _ _ _ _ _ _ Host_Cartesian _ _ K_bin K_premonoidal.
  63
  64   Definition K_enrichment : Enrichment.
  65     refine
  66       {| enr_c_pm  := K_premonoidal
  67        ; enr_v_mon := MonoidalFullSubcategory_Monoidal Host_Cartesian _ _ VK
  68       |}.
  69       Defined.
  70
  71   Instance ArrowsAreGeneralizedArrows : GeneralizedArrow K_enrichment (TypesEnrichedInJudgments Host) :=
  72     { ga_functor_monoidal :=
  73         PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed Host_Cartesian }.
  74
  75 End ArrowInLanguage.