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 ProgrammingLanguage.
34 Require Import ProgrammingLanguageGeneralizedArrow.
35 Require Import FreydCategories.
37 Require Import GeneralizedArrow.
39 Section ArrowInLanguage.
41 (* an Arrow In A Programming Language consists of... *)
43 (* a host language: *)
44 Context `(Host:ProgrammingLanguage).
46 (* ... for which Types(L) is cartesian: *)
47 Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)).
49 (* along with a full subcategory of Z(Types(L)) *)
50 Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P).
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)).
55 PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed.
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).
63 Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC))
64 Context (K :@PreMonoidalCat _ _ KE kbo kbc ).
65 Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))).
67 Definition ArrowInProgrammingLanguage :=
68 @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K.
70 Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
71 refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.