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 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.
27 Require Import NaturalDeduction.
28 Require Import NaturalDeductionCategory.
30 Require Import Enrichments.
31 Require Import Reification.
32 Require Import GeneralizedArrow.
33 Require Import ProgrammingLanguageEnrichment.
35 Section ProgrammingLanguageGeneralizedArrow.
38 `(Guest : ProgrammingLanguage)
39 `(Host : ProgrammingLanguage)
40 (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
41 (HostMonic : MonicEnrichment (TypesEnrichedInJudgments Host)).
43 Definition GeneralizedArrowInLanguage
44 := GeneralizedArrow (TypesEnrichedInJudgments Guest) HostMonoidal.
46 End ProgrammingLanguageGeneralizedArrow.