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

diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v
index 620ca9f..bac2397 100644
--- a/src/ProgrammingLanguageGeneralizedArrow.v
+++ b/src/ProgrammingLanguageGeneralizedArrow.v
@@ -29,34 +29,20 @@ Require Import NaturalDeductionCategory.
 
 Require Import FreydCategories.
 
+Require Import Reification.
+Require Import GeneralizedArrow.
 Require Import GeneralizedArrowFromReification.
-Section GArrowInLanguage.
+Require Import ProgrammingLanguage.
 
-  Definition GeneralizedArrowInLanguage (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME)
-    := GeneralizedArrow Guest Host.
-
-  Definition ArrowsAreGeneralizedArrows (Host:ProgrammingLanguageSMME)
-    {mf}{mn}{cc}{kehom}{CC}
-    (arrow:ArrowInProgrammingLanguage Host _ _ CC mf mn cc kehom) :  GeneralizedArrowInLanguage.
-
-  Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
+Require Import ReificationsAndGeneralizedArrows.
+Require Import ReificationFromGeneralizedArrow.
 
-  Context (GuestHost:TwoLevelLanguage).
+Section ProgrammingLanguageGeneralizedArrow.
 
-  Definition FlatObject (x:TypesL _ _ Host) :=
-    forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
+  Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
 
-  Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
-
-  Section Flattening.
-
-    Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
-    Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
-    Lemma FlatteningIsNotDestructive : 
-      FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ~~~~ GuestHost.
-      admit.
-      Qed.
+  Definition GeneralizedArrowInLanguage 
+    := GeneralizedArrow Guest Host.
 
-  End Flattening.
+End ProgrammingLanguageGeneralizedArrow.
 
-End GArrowInLanguage.