1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguageArrow *)
4 (* Arrows in ProgrammingLanguages. *)
6 (*********************************************************************************************************************************)
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.
30 Require Import NaturalDeduction.
31 Require Import NaturalDeductionCategory.
33 Require Import ProgrammingLanguageCategory.
34 Require Import FreydCategories.
35 Require Import Enrichments.
36 Require Import GeneralizedArrow.
38 Section ArrowInLanguage.
40 (* an Arrow In A Programming Language consists of... *)
42 (* a host language: *)
43 Context `(Host : ProgrammingLanguage).
45 Context (Host_Monoidal : MonoidalCat (TypesL_PreMonoidal Host)).
46 Context (Host_Cartesian : CartesianCat Host_Monoidal).
51 (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
53 Context (VK : FullSubcategory Host_Cartesian P).
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))).
59 Context (K_premonoidal:PreMonoidalCat K_bin (one(TerminalObject:=Host_Cartesian))).
61 Definition ArrowInProgrammingLanguage :=
62 @FreydCategory _ _ _ _ _ _ _ _ Host_Cartesian _ _ K_bin K_premonoidal.
64 Definition K_enrichment : Enrichment.
66 {| enr_c_pm := K_premonoidal
67 ; enr_v_mon := MonoidalFullSubcategory_Monoidal Host_Cartesian _ _ VK
71 Instance ArrowsAreGeneralizedArrows : GeneralizedArrow K_enrichment (TypesEnrichedInJudgments Host) :=
72 { ga_functor_monoidal :=
73 PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed Host_Cartesian }.