X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongCategory.v;fp=src%2FHaskStrongCategory.v;h=abbdc7206619beee74fc48ffecbf52d267897a81;hp=99772c72ab0bbaf76415a820f835f4029970e812;hb=85e4f0fd6b0673c1cc763eeb2585b7dc3d388455;hpb=70939a4eb9560ceeea3e9cf176ac5a36f9201ac4

diff --git a/src/HaskStrongCategory.v b/src/HaskStrongCategory.v
index 99772c7..abbdc72 100644
--- a/src/HaskStrongCategory.v
+++ b/src/HaskStrongCategory.v
@@ -1,7 +1,7 @@
 (*********************************************************************************************************************************)
 (* HaskStrongCategory:                                                                                                           *)
 (*                                                                                                                               *)
-(*    Well-typed Haskell terms in a specific tyvar/covar context form a category                                                 *)
+(*    Well-typed Haskell terms in a specific tyvar/covar context form a category:  Types(Haskell)                                *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
@@ -17,16 +17,15 @@ Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 
+(* the category of flat Haskell terms in a specific Γ Δ context *)
 (*  
-    (* the category of flat Haskell terms (n-ary) *)
-    Section HaskFlat.
-  
-      Context (past:@Past V).
+Section HaskFlat.
+  Context (Γ:TypeEnv)(Δ:CoercionEnv Γ).
     
-      Lemma idmor   a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
-        (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
-        admit.
-        Defined.
+  Lemma idmor   a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
+  (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
+    admit.
+  Defined.
     
       Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
         admit.
@@ -125,3 +124,4 @@ Require Import HaskStrong.
 *)  
 
 
+