From c3b1fb9622a65ad01e54b6e35785cee672d25bdc Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 4 Apr 2011 02:53:27 +0000 Subject: [PATCH] update to account for coq-categories changes --- src/Enrichments.v | 97 +++++++++++ src/ExtractionMain.v | 5 +- src/HaskProofFlattener.v | 4 +- src/NaturalDeduction.v | 17 +- src/NaturalDeductionCategory.v | 300 +++++++++++++++++++++-------------- src/ProgrammingLanguage.v | 62 ++++++-- src/ProgrammingLanguageArrow.v | 2 + src/ProgrammingLanguageFlattening.v | 10 +- src/Reification.v | 3 + src/categories | 2 +- 10 files changed, 356 insertions(+), 146 deletions(-) create mode 100644 src/Enrichments.v diff --git a/src/Enrichments.v b/src/Enrichments.v new file mode 100644 index 0000000..f78415d --- /dev/null +++ b/src/Enrichments.v @@ -0,0 +1,97 @@ +(*********************************************************************************************************************************) +(* Enrichments *) +(* *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +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 BinoidalCategories. +Require Import PreMonoidalCategories. + +(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *) +(* +Definition SurjectiveEnrichment `(ec:ECategory(Hom:=Vhom)(V:=V)(bin_obj':=Vbobj)(EI:=EI)) := + @treeDecomposition _ _ + (fun t => match t with + | None => EI + | Some x => match x with pair y z => Vhom y z end + end) + bin_obj. +*) + +(* in the paper this is called simply an "enrichment" *) +Structure PreMonoidalEnrichment := +{ enr_v_ob : Type +; enr_v_hom : enr_v_ob -> enr_v_ob -> Type +; enr_v : Category enr_v_ob enr_v_hom +; enr_v_i : enr_v_ob +; enr_v_bobj : enr_v -> enr_v -> enr_v +; enr_v_bin : BinoidalCat enr_v enr_v_bobj +; enr_v_pmon : PreMonoidalCat enr_v_bin enr_v_i +; enr_v_mon : MonoidalCat enr_v_pmon +; enr_c_obj : Type +; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v +; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom +; enr_c_bin : EBinoidalCat enr_c +; enr_c_i : enr_c +; enr_c_pm : PreMonoidalCat enr_c_bin enr_c_i +}. +Coercion enr_c : PreMonoidalEnrichment >-> ECategory. + +(* +Structure MonoidalEnrichment {e:Enrichment} := +{ me_enr :=e +; me_fobj : prod_obj e e -> e +; me_f : Functor (e ×× e) e me_fobj +; me_i : e +; me_mon : MonoidalCat e me_fobj me_f me_i +; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i) +}. +Implicit Arguments MonoidalEnrichment [ ]. +Coercion me_mon : MonoidalEnrichment >-> MonoidalCat. +Coercion me_enr : MonoidalEnrichment >-> Enrichment. + +(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *) +Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} := +{ ffme_enr := me +; ffme_mf_full : FullFunctor (HomFunctor e (me_i me)) +; ffme_mf_faithful : FaithfulFunctor (HomFunctor e (me_i me)) +; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me)) +}. +Implicit Arguments MonicMonoidalEnrichment [ ]. +Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment. +Transparent HomFunctor. + +Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) := +{ smme_se : SurjectiveEnrichment e +; smme_monoidal : MonoidalEnrichment e +; smme_me : MonicMonoidalEnrichment _ smme_monoidal +}. +Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment. +Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment. + +(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *) +Structure SMME := +{ smme_e : Enrichment +; smme_see : SurjectiveEnrichment smme_e +; smme_mon : MonoidalEnrichment smme_e +; smme_mee : MonicMonoidalEnrichment _ smme_mon +}. +Coercion smme_e : SMME >-> Enrichment. +Coercion smme_see : SMME >-> SurjectiveEnrichment. +Coercion smme_mon : SMME >-> MonoidalEnrichment. +Coercion smme_mee : SMME >-> MonicMonoidalEnrichment. +*) \ No newline at end of file diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 02643e5..f7f47a3 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -37,7 +37,6 @@ Require Import ProgrammingLanguage. Require Import HaskProofFlattener. Require Import HaskProofStratified. -Require Import HaskProofCategory. Require Import ReificationsIsomorphicToGeneralizedArrows. @@ -118,7 +117,7 @@ Section core2proof. "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++ "\usepackage[tightpage,active]{preview}"+++eol+++ "\begin{document}"+++eol+++ - "\setlength\PreviewBorder{5pt}"+++eol+++. + "\setlength\PreviewBorder{5pt}"+++eol. Definition footer : string := eol+++"\end{document}"+++ @@ -137,7 +136,7 @@ Section core2proof. addErrorMessage ("HaskType: " +++ toString τ) ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e => OK (eol+++eol+++eol+++ - "\begin{preview}"+++eol + "\begin{preview}"+++eol+++ "$\displaystyle "+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++ " $"+++eol+++ diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v index c37079f..d0d8b84 100644 --- a/src/HaskProofFlattener.v +++ b/src/HaskProofFlattener.v @@ -30,6 +30,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. @@ -138,7 +140,7 @@ Section HaskProofFlattener. set (@nil (HaskTyVar Γ ★)) as lev. - unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros. + unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros. induction X; simpl. diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index ced66c4..74ecaef 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -248,6 +248,11 @@ Section Natural_Deduction. (* products and duplication must distribute over each other *) ; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b + ; ndr_comp_preserves_cancell : forall `(f:a/⋯⋯/b), nd_cancell;; f === nd_id _ ** f ;; nd_cancell + ; ndr_comp_preserves_cancelr : forall `(f:a/⋯⋯/b), nd_cancelr;; f === f ** nd_id _ ;; nd_cancelr + ; ndr_comp_preserves_assoc : forall `(f:a/⋯⋯/b)`(g:a1/⋯⋯/b1)`(h:a2/⋯⋯/b2), + nd_assoc;; (f ** (g ** h)) === ((f ** g) ** h) ;; nd_assoc + (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *) ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g @@ -377,12 +382,12 @@ Section Natural_Deduction. (* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules * mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *) Class TreeStructuralRules := - { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x] - ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x] - ; tsr_ant_cancell : forall {x a }, ND [ [],,a |= x] [ a |= x] - ; tsr_ant_cancelr : forall {x a }, ND [a,,[] |= x] [ a |= x] - ; tsr_ant_llecnac : forall {x a }, ND [ a |= x] [ [],,a |= x] - ; tsr_ant_rlecnac : forall {x a }, ND [ a |= x] [ a,,[] |= x] + { tsr_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x] + ; tsr_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x] + ; tsr_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x] + ; tsr_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x] + ; tsr_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x] + ; tsr_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x] }. Notation "[# a #]" := (nd_rule a) : nd_scope. diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 0a82aa2..fd352e1 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -14,7 +14,6 @@ Require Import Algebras_ch4. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. -Require Import ProductCategories_ch1_6_1. Require Import OppositeCategories_ch1_6_2. Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. @@ -54,29 +53,45 @@ Section Judgments_Category. intros; apply ndr_comp_associativity. Defined. - (* it is monoidal, with the judgment-tree-formation operator as its tensor *) - Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category := - fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy). - Definition Judgments_Category_monoidal_endofunctor_fmor : - forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) -> - ((Judgments_Category_monoidal_endofunctor_fobj a) - ~~{Judgments_Category}~~> - (Judgments_Category_monoidal_endofunctor_fobj b)). - intros. - destruct a. - destruct b. - destruct X. - simpl in *. - exact (h**h0). - Defined. - Definition Judgments_Category_monoidal_endofunctor - : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj. - refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl. - abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto). - abstract (destruct a; simpl in *; reflexivity). - abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp). - Defined. + Hint Extern 1 => apply nd_structural_id0. + Hint Extern 1 => apply nd_structural_id1. + Hint Extern 1 => apply nd_structural_weak. + Hint Extern 1 => apply nd_structural_copy. + Hint Extern 1 => apply nd_structural_prod. + Hint Extern 1 => apply nd_structural_comp. + Hint Extern 1 => apply nd_structural_cancell. + Hint Extern 1 => apply nd_structural_cancelr. + Hint Extern 1 => apply nd_structural_llecnac. + Hint Extern 1 => apply nd_structural_rlecnac. + Hint Extern 1 => apply nd_structural_assoc. + Hint Extern 1 => apply nd_structural_cossa. + Hint Extern 1 => apply weak'_structural. + Instance jud_first (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => x,,a) := + { fmor := fun b c (f:b /⋯⋯/ c) => f ** (nd_id a) }. + intros; unfold eqv; simpl. + apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *. + reflexivity. + intros; unfold eqv in *; simpl in *. + setoid_rewrite <- ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + reflexivity. + Defined. + Instance jud_second (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => a,,x) := + { fmor := fun b c (f:b /⋯⋯/ c) => (nd_id a) ** f }. + intros; unfold eqv; simpl. + apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *. + reflexivity. + intros; unfold eqv in *; simpl in *. + setoid_rewrite <- ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + reflexivity. + Defined. + Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) := + { bin_first := jud_first + ; bin_second := jud_second }. Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)). refine {| iso_forward := nd_assoc @@ -95,114 +110,163 @@ Section Judgments_Category. ; iso_backward := nd_llecnac |}; abstract (simpl; auto). Defined. - - Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. - refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl. - abstract (setoid_rewrite (ndr_prod_right_identity f); - repeat setoid_rewrite ndr_comp_associativity; - apply ndr_comp_respects; try reflexivity; - symmetry; - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]; - apply ndr_comp_respects; try reflexivity; simpl; auto). + Instance jud_mon_cancelr : jud_first [] <~~~> functor_id Judgments_Category := + { ni_iso := jud_cancelr_iso }. + intros; unfold eqv in *; simpl in *. + apply ndr_comp_preserves_cancelr. Defined. - Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. - eapply Build_NaturalIsomorphism. - instantiate (1:=fun x => jud_cancell_iso x). - abstract (intros; simpl; - setoid_rewrite (ndr_prod_left_identity f); - repeat setoid_rewrite ndr_comp_associativity; - apply ndr_comp_respects; try reflexivity; - symmetry; - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]; - apply ndr_comp_respects; try reflexivity; simpl; auto). + Instance jud_mon_cancell : jud_second [] <~~~> functor_id Judgments_Category := + { ni_iso := jud_cancell_iso }. + intros; unfold eqv in *; simpl in *. + apply ndr_comp_preserves_cancell. Defined. - Definition jud_mon_assoc_iso : forall X, - (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> - Judgments_Category_monoidal_endofunctor) X) ≅ - (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> - Judgments_Category_monoidal_endofunctor))) X. - intros. - destruct X as [a c]. - destruct a as [a b]. - exact (jud_assoc_iso a b c). + Instance jud_mon_assoc : forall a b, a ⋊- >>>> - ⋉b <~~~> - ⋉b >>>> a ⋊- := + { ni_iso := fun c => jud_assoc_iso a c b }. + intros; unfold eqv in *; simpl in *. + apply ndr_comp_preserves_assoc. Defined. - Definition jud_mon_assoc : - ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) - <~~~> - func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)). - refine {| ni_iso := jud_mon_assoc_iso |}. + Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b. intros. - unfold hom in *. - destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *. - destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *. - destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *. - unfold hom in *. - unfold ob in *. - unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl. - setoid_rewrite ndr_prod_associativity. - setoid_rewrite ndr_comp_associativity. - setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - etransitivity. - symmetry. - apply ndr_comp_right_identity. - apply ndr_comp_respects; try reflexivity. - apply ndr_structural_indistinguishable; auto. + apply ni_inv. + refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}. + intros; unfold eqv in *; simpl in *. + apply ndr_comp_preserves_assoc. Defined. - - Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] := - { mon_cancelr := jud_mon_cancelr - ; mon_cancell := jud_mon_cancell - ; mon_assoc := jud_mon_assoc }. - abstract - (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl; - apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto). - abstract - (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl; - apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto). + Instance jud_mon_assoc_ll : forall a b, (a ⊗ b) ⋊- <~~~> b ⋊- >>>> a ⋊- := + { ni_iso := fun c => jud_assoc_iso _ _ _ }. + intros; unfold eqv in *; simpl in *. + apply ndr_comp_preserves_assoc. Defined. - Instance Judgments_Category_Terminal : Terminal Judgments_Category. - refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}. + Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] := + { pmon_cancelr := jud_mon_cancelr + ; pmon_cancell := jud_mon_cancell + ; pmon_assoc := jud_mon_assoc + ; pmon_assoc_rr := jud_mon_assoc_rr + ; pmon_assoc_ll := jud_mon_assoc_ll + }. + unfold functor_fobj; unfold fmor; simpl; + apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto. + + unfold functor_fobj; unfold fmor; simpl; + apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto. + + intros; unfold eqv; simpl; auto. + + intros; unfold eqv; simpl; auto. + + intros; unfold eqv; simpl. + apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + + intros; unfold eqv; simpl. + apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + + intros; unfold eqv; simpl. + apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + symmetry. + etransitivity; [ idtac | apply ndr_prod_preserves_comp ]. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + apply ndr_prod_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. + + Defined. + + Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal. + apply Build_MonoidalCat. + apply Build_CommutativeCat. + intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *. + + setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)). + setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g). + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + + setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)). + setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f). + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + Defined. + + Instance Judgments_Category_Terminal : TerminalObject Judgments_Category []. + refine {| drop := nd_weak' ; drop_unique := _ |}. abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant). Defined. Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal. - refine {| copy_nt := _ |}. intros. - refine {| nt_component := nd_copy |}. - intros. - unfold hom in *; unfold ob in *; unfold eqv. - simpl. - rewrite ndr_prod_preserves_copy; auto. - reflexivity. - Defined. + refine {| copy := nd_copy |}; intros; simpl. + setoid_rewrite ndr_comp_associativity. + setoid_rewrite <- (ndr_prod_preserves_copy f). + apply ndr_comp_respects; try reflexivity. + etransitivity. + symmetry. + apply ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + setoid_rewrite ndr_comp_associativity. + setoid_rewrite <- (ndr_prod_preserves_copy f). + apply ndr_comp_respects; try reflexivity. + etransitivity. + symmetry. + apply ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + Defined. + + Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal := + { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }. - Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal. - refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal - ; car_one := iso_id [] |} - ; intros; unfold hom; simpl - ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl. - - apply ndr_structural_indistinguishable; auto. - apply nd_structural_comp; auto. - apply nd_structural_comp; auto. - unfold copy; simpl; apply nd_structural_copy; auto. - apply nd_structural_prod; auto. - apply nd_structural_comp; auto. - apply weak'_structural. - apply nd_structural_id0; auto. - apply nd_structural_cancell; auto. - - apply ndr_structural_indistinguishable; auto. - apply nd_structural_comp; auto. - apply nd_structural_comp; auto. - unfold copy; simpl; apply nd_structural_copy; auto. - apply nd_structural_prod; auto. - apply nd_structural_comp; auto. - apply weak'_structural. - apply nd_structural_id0; auto. - apply nd_structural_cancelr; auto. + intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl. + apply ndr_structural_indistinguishable; auto. + intros; unfold hom; simpl; unfold functor_fobj; unfold fmor; simpl. + apply ndr_structural_indistinguishable; auto. Defined. End Judgments_Category. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index c9f8352..7831fad 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -73,13 +73,14 @@ Section Programming_Language. apply pl_subst. Defined. + Existing Instance pl_eqv. Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). refine {| eid := identityProof ; ecomp := cutProof |}; intros. - apply MonoidalCat_all_central. - apply MonoidalCat_all_central. + apply (mon_commutative(MonoidalCat:=JudgmentsL)). + apply (mon_commutative(MonoidalCat:=JudgmentsL)). unfold identityProof; unfold cutProof; simpl. apply nd_cut_left_identity. unfold identityProof; unfold cutProof; simpl. @@ -91,7 +92,7 @@ Section Programming_Language. Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ). refine {| efunc := fun x y => (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y) |}. - intros; apply MonoidalCat_all_central. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. apply se_reflexive_right. intros. unfold ehom. unfold comp. simpl. unfold cutProof. @@ -105,7 +106,7 @@ Section Programming_Language. Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x). eapply Build_EFunctor. instantiate (1:=(fun x y => ((@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))). - intros; apply MonoidalCat_all_central. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. apply se_reflexive_left. intros. unfold ehom. unfold comp. simpl. unfold cutProof. @@ -123,23 +124,52 @@ Section Programming_Language. |}. Defined. - Definition Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a. + Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) := + { iso_forward := nd_seq_reflexive _ ;; tsr_ant_cossa _ a b c + ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_assoc _ a b c + }. + admit. + admit. + Defined. + + Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a c b }. + admit. + Defined. + + Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a := + { iso_forward := nd_seq_reflexive _ ;; tsr_ant_rlecnac _ a + ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_cancelr _ a + }. + admit. admit. Defined. - Definition Types_cancelr : Types_first [] <~~~> functor_id _. + Instance Types_cancelr : Types_first [] <~~~> functor_id _ := + { ni_iso := Types_cancelr_iso }. admit. Defined. - Definition Types_cancell : Types_second [] <~~~> functor_id _. + Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a := + { iso_forward := nd_seq_reflexive _ ;; tsr_ant_llecnac _ a + ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_cancell _ a + }. + admit. admit. Defined. - Definition Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a. + Instance Types_cancell : Types_second [] <~~~> functor_id _ := + { ni_iso := Types_cancell_iso }. admit. Defined. - Definition Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b. + Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a b c }. + admit. + Defined. + + Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b := + { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }. admit. Defined. @@ -152,10 +182,14 @@ Section Programming_Language. }. admit. (* pentagon law *) admit. (* triangle law *) - admit. (* assoc_rr/assoc coherence *) - admit. (* assoc_ll/assoc coherence *) + intros; simpl; reflexivity. + intros; simpl; reflexivity. + admit. (* assoc central *) + admit. (* cancelr central *) + admit. (* cancell central *) Defined. + (* Definition TypesEnrichedInJudgments : Enrichment. refine {| enr_c := TypesL |}. Defined. @@ -172,11 +206,11 @@ Section Programming_Language. Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments. admit. Defined. - + *) End LanguageCategory. End Programming_Language. - +(* Structure ProgrammingLanguageSMME := { plsmme_t : Type ; plsmme_judg : Type @@ -187,5 +221,5 @@ Structure ProgrammingLanguageSMME := }. Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage. Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment. - +*) Implicit Arguments ND [ Judgment ]. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index 40bc164..a4f40e3 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -117,6 +117,7 @@ Section MonoidalSubCat. End MonoidalSubCat. Coercion full_subcat_is_monoidal : MonoidalSubCat >-> MonoidalCat. +(* Section ArrowInLanguage. (* an Arrow In A Programming Language consists of... *) @@ -162,3 +163,4 @@ Check (@FreydCategory). Defined. End GArrowInLanguage. +*) \ No newline at end of file diff --git a/src/ProgrammingLanguageFlattening.v b/src/ProgrammingLanguageFlattening.v index a4bf015..f01621b 100644 --- a/src/ProgrammingLanguageFlattening.v +++ b/src/ProgrammingLanguageFlattening.v @@ -24,13 +24,16 @@ Require Import FunctorCategories_ch7_7. Require Import Reification. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. +Require Import GeneralizedArrow. +Require Import GeneralizedArrowFromReification. Require Import ProgrammingLanguage. -Require Import ProgrammingReification. +Require Import ProgrammingLanguageReification. +Require Import ReificationsAndGeneralizedArrows. Section Flattening. Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME). - Context (GuestHost:TwoLevelLanguage). + Context (GuestHost:TwoLevelLanguage Guest Host). Definition FlatObject (x:TypesL _ _ Host) := forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). @@ -42,6 +45,7 @@ Section Flattening. Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F. +(* Lemma FlatteningIsNotDestructive : FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ≃ GuestHost. apply if_inv. @@ -65,7 +69,7 @@ Section Flattening. apply if_inv. apply retraction_composes. Qed. - +*) End Flattening. diff --git a/src/Reification.v b/src/Reification.v index f60c43e..2b9aac9 100644 --- a/src/Reification.v +++ b/src/Reification.v @@ -18,8 +18,11 @@ 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 Enrichments. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. diff --git a/src/categories b/src/categories index 2160781..e928451 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit 21607813788d83fb58ce128df442a4ee3edfbdaf +Subproject commit e928451c4c45cdbdd975bbfb229e8cc2616b8194 -- 1.7.10.4