From d1a4d10de986d774d3cfb10348036cb60bc80277 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 2 Apr 2011 15:49:20 -0700 Subject: [PATCH] update submodule pointer, account for changes upstream --- src/All.v | 3 +-- src/GeneralizedArrowCategory.v | 2 ++ src/GeneralizedArrowFromReification.v | 2 ++ src/NaturalDeductionCategory.v | 4 +++- src/ProgrammingLanguage.v | 2 ++ src/ProgrammingLanguageArrow.v | 18 +++++++++++++----- src/categories | 2 +- 7 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/All.v b/src/All.v index d9f1d16..b42d175 100644 --- a/src/All.v +++ b/src/All.v @@ -79,8 +79,7 @@ Require Import GeneralizedArrowCategory. Require Import ReificationsAndGeneralizedArrows. Require Import ReificationsIsomorphicToGeneralizedArrows. -Require Import HaskProofStratified. -Require Import HaskProofFlattener. +Require Import HaskProofCategory. Require Import ProgrammingLanguage. (* very slow! *) diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index 7d8b20b..28b7555 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -18,6 +18,8 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 4a9e790..15d1b09 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -17,6 +17,8 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 0a413e7..0a82aa2 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -20,9 +20,11 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. -Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import InitialTerminal_ch2_2. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch7_8. Open Scope nd_scope. Open Scope pf_scope. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 5ce624f..c9f8352 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -18,6 +18,8 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index f4a0d8e..40bc164 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -122,7 +122,7 @@ Section ArrowInLanguage. (* an Arrow In A Programming Language consists of... *) (* a host language: *) - Context (Host:ProgrammingLanguageSMME). + Context `(Host:ProgrammingLanguage). (* ... for which Types(L) is cartesian: *) Context {MF}(center_of_TypesL:MonoidalCat (TypesL _ _ Host) (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []). @@ -131,13 +131,20 @@ Section ArrowInLanguage. Context (VK:MonoidalSubCat center_of_TypesL). (* a premonoidal category enriched in aforementioned full subcategory *) - Context {Kehom:center_of_TypesL -> center_of_TypesL -> VK}. + Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK). +Check (@ECategory). + Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom). - Context {KE:@ECategory _ _ VK _ _ _ VK center_of_TypesL Kehom}. +Check (Underlying KE). - Context (CC:CartesianCat center_of_TypesL). + Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}. + + Context (kbc:@BinoidalCat center_of_TypesL _ (Underlying KE) kbo). - Context {kbo}{kbc}(K:@PreMonoidalCat _ _ KE kbo kbc (@one _ _ _ (car_terminal(CartesianCat:=CC)))). + Check (@PreMonoidalCat) + Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC)) + Context (K:@PreMonoidalCat _ _ KE kbo kbc ). + Context (CC:CartesianCat center_of_TypesL). (* Definition K_enrichment : Enrichment. @@ -145,6 +152,7 @@ Section ArrowInLanguage. Defined. Context (K_surjective:SurjectiveEnrichment K_enrichment). *) +Check (@FreydCategory). Definition ArrowInProgrammingLanguage := @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K. diff --git a/src/categories b/src/categories index a0b31d2..2160781 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit a0b31d2cc2b6cf7184efe4ff01ad682749f779ad +Subproject commit 21607813788d83fb58ce128df442a4ee3edfbdaf -- 1.7.10.4