X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguageGeneralizedArrow.v;h=8fe0391c19affafe821d2a957226c029eae3145f;hp=bac2397ea148f86a0fa8179f35a6f261e356af18;hb=034f7e7856bebbbcb3c83946aa603c640b17f3bb;hpb=e68b13536be2d1def208bde68dbbcdc4c1097d16

diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v
index bac2397..8fe0391 100644
--- a/src/ProgrammingLanguageGeneralizedArrow.v
+++ b/src/ProgrammingLanguageGeneralizedArrow.v
@@ -27,22 +27,21 @@ Require Import FunctorCategories_ch7_7.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 
-Require Import FreydCategories.
-
+Require Import Enrichments.
 Require Import Reification.
 Require Import GeneralizedArrow.
-Require Import GeneralizedArrowFromReification.
-Require Import ProgrammingLanguage.
-
-Require Import ReificationsAndGeneralizedArrows.
-Require Import ReificationFromGeneralizedArrow.
+Require Import ProgrammingLanguageEnrichment.
 
 Section ProgrammingLanguageGeneralizedArrow.
 
-  Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
+  Context
+  `(Guest        : ProgrammingLanguage)
+  `(Host         : ProgrammingLanguage)
+   (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
+   (HostMonic    : MonicEnrichment    (TypesEnrichedInJudgments Host)).
 
   Definition GeneralizedArrowInLanguage 
-    := GeneralizedArrow Guest Host.
+    := GeneralizedArrow (TypesEnrichedInJudgments Guest) HostMonoidal.
 
 End ProgrammingLanguageGeneralizedArrow.