lots of cleanup

[coq-hetmet.git] / src / HaskStrongCategory.v

diff --git a/src/HaskStrongCategory.v b/src/HaskStrongCategory.v
deleted file mode 100644 (file)
index abbdc72..0000000
--- a/src/HaskStrongCategory.v
+++ /dev/null
@@ -1,127 +0,0 @@
-(*********************************************************************************************************************************)
-(* HaskStrongCategory:                                                                                                           *)
-(*                                                                                                                               *)
-(*    Well-typed Haskell terms in a specific tyvar/covar context form a category:  Types(Haskell)                                *)
-(*                                                                                                                               *)
-(*********************************************************************************************************************************)
-
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
-Require Import HaskKinds.
-Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
-Require Import HaskStrongTypes.
-Require Import HaskStrong.
-
-(* the category of flat Haskell terms in a specific Γ Δ context *)
-(*  
-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 compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
-        admit.
-        Defined.
-      
-      Definition HaskFlat
-        : ECategory
-            (SystemFC_Cat_Flat past)
-            (Tree ??(@CoreType V))
-            (fun a s => [(a,s)]).
-        refine
-          {| eid   := fun a     => idmor   a
-           ; ecomp := fun a b c => compmor a b c
-          |}; intros; simpl in *; auto.
-        apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
-        apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
-        admit.
-        admit.
-        admit.
-        Defined.
-  
-      Definition HaskFlatEnrichment : SurjectiveEnrichment.
-        refine {| se_enr := {| enr_c := HaskFlat |} |}.
-        admit.
-        Defined.
-  
-    End HaskFlat.
-  
-    (* the category of multi-level Haskell terms (n-ary) with a given past *)
-    Section Hask.
-      Context (past:@Past V).
-  
-      Lemma idmor'   a : [] ~~{SystemFC_Cat 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 past}~~> [(a,c)].
-        admit.
-        Defined.
-  
-      Definition Hask
-        : ECategory
-            (SystemFC_Cat past)
-            (Tree ??(@LeveledHaskType V))
-            (fun a s => [(a,s)]).
-        refine
-          {| eid   := fun a     => idmor'   a
-           ; ecomp := fun a b c => compmor' a b c
-          |}; intros; simpl in *; auto.
-        apply (MonoidalCat_all_central (SystemFC_Cat past)).
-        apply (MonoidalCat_all_central (SystemFC_Cat past)).
-        admit.
-        admit.
-        admit.
-        Defined.
-  
-      Definition HaskEnrichmentMonoidal : MonoidalEnrichment.
-        refine {| me_enr := {| enr_c := Hask |} |}.
-        Admitted.
-  
-      Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment.
-        refine {| ffme_enr := HaskEnrichmentMonoidal |}.
-        admit.
-        admit.
-        admit.
-        Defined.
-    End Hask.
-  
-    Section ReificationAndGeneralizedArrow.
-      Context
-        (past:list ((Tree ??(@LeveledHaskType V)) * V))
-        (Σ:(Tree ??(@LeveledHaskType V)))
-        (n:V).
-    
-      Definition SystemFC_Reification 
-        : Reification
-        (HaskFlatEnrichment (((Σ,n)::past))) 
-        (HaskEnrichmentMonicMonoidal  (*past*))
-        (me_i (HaskEnrichmentMonicMonoidal (*past*))).
-        (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*)
-        admit.
-        Defined.
-(*    
-      Definition SystemFC_GArrow :=
-        garrow_from_reification
-        (HaskFlatEnrichment (((Σ,n)::past)))
-        (HaskEnrichmentMonicMonoidal (*past*))
-        SystemFC_Reification.
-  *)
-      (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor;
-       * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory
-       * of Hask which consists of the (GArrow g => g a b) morphisms *)
-    
-    End ReificationAndGeneralizedArrow.
-*)  
-
-
-