From: Adam Megacz Date: Sun, 10 Apr 2011 04:04:51 +0000 (+0000) Subject: update to new coq-categories, base ND_Relation on inert sequences X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=64d416692bda1d36c33b5efa245d46dcf546ad4a;hp=562e94b529f34fb3854be7914a49190c5243c55a update to new coq-categories, base ND_Relation on inert sequences --- diff --git a/src/Enrichments.v b/src/Enrichments.v index f78415d..a98b047 100644 --- a/src/Enrichments.v +++ b/src/Enrichments.v @@ -20,78 +20,117 @@ Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import BinoidalCategories. Require Import PreMonoidalCategories. +Require Import PreMonoidalCenter. +Require Import RepresentableStructure_ch7_2. +Require Import WeakFunctorCategory. + +(* in the paper this is called simply an "enrichment" *) +Structure Enrichment := +{ 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 +; enr_c_center := Center enr_c_bin +; enr_c_center_mon := Center_is_Monoidal enr_c_pm +}. +Coercion enr_c : Enrichment >-> ECategory. + +Structure SurjectiveEnrichment := +{ senr_c_obj : Type +; senr_v_ob := Tree ??(senr_c_obj * senr_c_obj) +; senr_c_hom := fun (c1 c2:senr_c_obj) => [(c1, c2)] +; senr_v_hom : senr_v_ob -> senr_v_ob -> Type +; senr_v : Category senr_v_ob senr_v_hom +; senr_v_i := [] +; senr_v_bobj := @T_Branch (option (senr_c_obj * senr_c_obj)) +; senr_v_bin : BinoidalCat senr_v senr_v_bobj +; senr_v_pmon : PreMonoidalCat senr_v_bin senr_v_i +; senr_v_mon : MonoidalCat senr_v_pmon +; senr_c : ECategory senr_v_mon senr_c_obj senr_c_hom +; senr_c_bin : EBinoidalCat senr_c +; senr_c_i : senr_c +; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i +}. + +Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment. +refine +{| enr_v_ob := senr_v_ob se +; enr_v_hom := senr_v_hom se +; enr_v := senr_v se +; enr_v_i := senr_v_i se +; enr_v_bobj := senr_v_bobj se +; enr_v_bin := senr_v_bin se +; enr_v_pmon := senr_v_pmon se +; enr_v_mon := senr_v_mon se +; enr_c_obj := senr_c_obj se +; enr_c_hom := senr_c_hom se +; enr_c := senr_c se +; enr_c_bin := senr_c_bin se +; enr_c_i := senr_c_i se +; enr_c_pm := senr_c_pm se +|}. +Defined. +Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment. -(* 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. +Definition MonoidalEnrichment (e:Enrichment) := + PreMonoidalFunctor + (enr_c_center_mon e) + (enr_v_pmon e) + (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))). *) +Definition MonoidalEnrichment (e:Enrichment) := + PreMonoidalFunctor + (enr_c_pm e) + (enr_v_pmon e) + (HomFunctor e (pmon_I (enr_c_pm e))). -(* 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. +(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *) (* -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. +Definition SurjectiveEnrichment (ec:Enrichment) := + @treeDecomposition (enr_v ec) (option (ec*ec)) + (fun t => match t with + | None => enr_v_i ec + | Some x => match x with pair y z => enr_c_hom ec y z end + end) + (enr_v_bobj ec). +*) -(* 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)) +Class MonicEnrichment {e:Enrichment} := +{ me_enr := e +; me_homfunctor := HomFunctor e (enr_c_i e) +(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*) +; me_full : FullFunctor me_homfunctor +; me_faithful : FaithfulFunctor me_homfunctor +; me_conservative : ConservativeFunctor me_homfunctor }. -Implicit Arguments MonicMonoidalEnrichment [ ]. -Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment. +Implicit Arguments MonicEnrichment [ ]. +Coercion me_enr : MonicEnrichment >-> Enrichment. 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_e : SurjectiveEnrichment +(*; smme_see : SurjectiveEnrichment smme_e*) ; smme_mon : MonoidalEnrichment smme_e -; smme_mee : MonicMonoidalEnrichment _ smme_mon +; smme_mee : MonicEnrichment smme_e }. -Coercion smme_e : SMME >-> Enrichment. -Coercion smme_see : SMME >-> SurjectiveEnrichment. +Coercion smme_e : SMME >-> SurjectiveEnrichment. Coercion smme_mon : SMME >-> MonoidalEnrichment. -Coercion smme_mee : SMME >-> MonicMonoidalEnrichment. -*) \ No newline at end of file + +Definition SMMEs : SmallCategories. + refine {| small_cat := SMME + ; small_cat_cat := fun smme => enr_v smme + |}. + Defined. diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v index bf7743b..9149734 100644 --- a/src/GeneralizedArrow.v +++ b/src/GeneralizedArrow.v @@ -20,14 +20,22 @@ Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. +Require Import PreMonoidalCenter. +Require Import PreMonoidalCategories. +Require Import BinoidalCategories. Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) := -{ ga_functor_obj : enr_v_mon K -> C -; ga_functor : Functor (enr_v_mon K) C ga_functor_obj -; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor +{ ga_functor_obj : enr_v K -> ce +; ga_functor : Functor (enr_v_mon K) (enr_c_pm ce) ga_functor_obj +; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor +(* +; ga_functor : Functor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj +; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor +*) }. -Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor. +Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor. Implicit Arguments GeneralizedArrow [ [ce] ]. Implicit Arguments ga_functor_obj [ K ce C ]. diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index 28b7555..3a6a74a 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -23,10 +23,10 @@ Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. Require Import GeneralizedArrow. Require Import WeakFunctorCategory. -Require Import SmallSMMEs. (* * Technically reifications form merely a *semicategory* (no identity @@ -49,28 +49,19 @@ Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type := Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 := match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with | gaoi_id s => fun x => x - | gaoi_ga s1 s2 f => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a) + | gaoi_ga s1 s2 f => fun a => ehom(ECategory:=s2) (enr_c_i (smme_e s2)) (ga_functor_obj f a) end. Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2) : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) := match f with | gaoi_id s => functor_id _ - | gaoi_ga s1 s2 f => ga_functor f >>>> HomFunctor s2 (mon_i s2) + | gaoi_ga s1 s2 f => ga_functor f >>>> HomFunctor s2 (enr_c_i s2) end. -Definition compose_generalizedArrows (s0 s1 s2:SMMEs) : - GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2. - intro g01. - intro g12. - refine - {| ga_functor := g01 >>>> HomFunctor s1 (mon_i s1) >>>> g12 |}. - apply MonoidalFunctorsCompose. - apply MonoidalFunctorsCompose. - apply (ga_functor_monoidal g01). - apply (me_mf s1). - apply (ga_functor_monoidal g12). - Defined. +Instance compose_generalizedArrows (s0 s1 s2:SMMEs) + (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 := + { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }. Definition generalizedArrowOrIdentityComp : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3. @@ -97,7 +88,6 @@ Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs. apply if_right_identity. unfold mf_F. idtac. - unfold mf_f. apply if_associativity. Defined. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 15d1b09..810e862 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -19,146 +19,536 @@ Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import BinoidalCategories. Require Import PreMonoidalCategories. +Require Import PreMonoidalCenter. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. Section GArrowFromReification. - Context `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)). + Definition binoidalcat_iso `{bc:BinoidalCat}{a1 b1 a2 b2:bc} (i1:a1≅a2)(i2:b1≅b2) : (a1⊗b1)≅(a2⊗b2) := + iso_comp + (functors_preserve_isos (- ⋉ b1) i1 ) + (functors_preserve_isos (a2 ⋊ -) i2). - Fixpoint garrow_fobj_ vk : C := + Context `(K : SurjectiveEnrichment) + `(CMon : MonicEnrichment C) + (CM : MonoidalEnrichment C) + (reification : Reification K C (pmon_I (enr_c_pm C))). + + Fixpoint garrow_fobj (vk:senr_v K) : C := match vk with - | T_Leaf None => me_i C + | T_Leaf None => enr_c_i C | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end - | t1,,t2 => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2)) + | t1,,t2 => bin_obj(BinoidalCat:=enr_c_bin C) (garrow_fobj t1) (garrow_fobj t2) end. - Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)). - - Definition homset_tensor_iso - : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk). - intros. - unfold garrow_fobj. - set (se_decomp _ K vk) as sevk. - destruct sevk. - simpl in *. - rewrite e. - clear e. - induction x; simpl. - - destruct a. - destruct p. - - apply iso_inv. - apply (ni_iso (reification_commutes reification e) e0). - - eapply id_comp. - apply iso_inv. - apply (mf_id (reification_rstar reification)). - apply (mf_id (me_mf C)). - - eapply id_comp. - apply iso_inv. - apply (ni_iso (mf_coherence (reification_rstar reification)) (pair_obj _ _)). - eapply id_comp. - Focus 2. - apply (ni_iso (mf_coherence (me_mf C)) (pair_obj _ _)). - unfold bin_obj. - apply (functors_preserve_isos (enr_v_f C) (a:=(pair_obj _ _))(b:=(pair_obj _ _))). - apply (iso_prod IHx1 IHx2). - Defined. - - Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (HomFunctor C (me_i C)). - exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)). - abstract (exists (garrow_fobj vk); auto). - Defined. + Fixpoint homset_tensor_iso (vk:enr_v_mon K) : reification vk ≅ enr_c_i C ~~> garrow_fobj vk := + match vk as VK return reification VK ≅ enr_c_i C ~~> garrow_fobj VK with + | T_Leaf None => (mf_i(PreMonoidalFunctor:=reification))⁻¹ >>≅>> (mf_i(PreMonoidalFunctor:=CM)) + | T_Leaf (Some a) => match a as A + return reification (T_Leaf (Some A)) ≅ enr_c_i C ~~> garrow_fobj (T_Leaf (Some A)) with + (s,s0) => iso_inv _ _ (ni_iso (reification_commutes reification s) s0) + end + | t1,,t2 => (ni_iso (@mf_first _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ reification _) _)⁻¹ >>≅>> + (binoidalcat_iso (homset_tensor_iso t1) (homset_tensor_iso t2)) >>≅>> + (ni_iso (mf_first(PreMonoidalFunctor:=CM) (garrow_fobj t2)) _) + end. - Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (HomFunctor C (me_i C))}~~>(garrow_fobj' b). - exists (iso_backward (homset_tensor_iso a) - >>> reification_rstar reification \ f - >>> iso_forward (homset_tensor_iso b)). - abstract (auto). - Defined. + Definition HomFunctor_fullimage := FullImage CM. - (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor + (* R' is a functor from the domain of the reification functor * to the full subcategory in the range of the [host language's] Hom(I,-) functor *) - Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'. - refine {| fmor := fun a b f => step1_mor f |}. - abstract (intros; unfold step1_mor; simpl; + Instance R' : Functor (FullImage (reification_rstar reification)) HomFunctor_fullimage garrow_fobj := + { fmor := fun a b (f:a~~{FullImage (reification_rstar reification)}~~>b) => + (#(homset_tensor_iso a)⁻¹ >>> f >>> #(homset_tensor_iso b)) + }. + abstract (intros; simpl; apply comp_respects; try reflexivity; apply comp_respects; try reflexivity; - apply fmor_respects; auto). - abstract (intros; unfold step1_mor; simpl; - setoid_rewrite fmor_preserves_id; + auto). + abstract (intros; simpl; setoid_rewrite right_identity; apply iso_comp2). abstract (intros; - unfold step1_mor; simpl; repeat setoid_rewrite <- associativity; apply comp_respects; try reflexivity; repeat setoid_rewrite associativity; - apply comp_respects; try reflexivity; - setoid_rewrite juggle2; - set (iso_comp1 (homset_tensor_iso b)) as qqq; - setoid_rewrite qqq; - clear qqq; - setoid_rewrite right_identity; - apply (fmor_preserves_comp reification)). + apply comp_respects; try apply reflexivity; + apply comp_respects; try apply reflexivity; + eapply transitivity; [ symmetry; apply associativity | idtac ]; + eapply transitivity; [ idtac | apply left_identity ]; + apply comp_respects; try apply reflexivity; + apply iso_comp1). Defined. - Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))). - exists (fun c1 => homset_tensor_iso c1). - abstract (intros; - simpl; - repeat setoid_rewrite <- associativity; - setoid_rewrite iso_comp1; - setoid_rewrite left_identity; - reflexivity). + (* the "step2_functor" is the section of the Hom(I,-) functor *) + Definition step2_functor := + ff_functor_section_functor _ (me_full(MonicEnrichment:=CMon)) (me_faithful(MonicEnrichment:=CMon)). + + Definition garrow_functor := + RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor). + + Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f. + simpl. + apply left_identity. Qed. - (* the "step2_functor" is the section of the Hom(I,-) functor *) - Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C). + Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f. + simpl. + apply right_identity. + Qed. - (* the generalized arrow is the composition of the two steps *) - Definition garrow_functor := step1_functor >>>> step2_functor. + Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f. + intros. + unfold ff_functor_section_fmor. + set (me_full a b f) as full. + destruct full. + apply e. + Qed. - Lemma garrow_functor_monoidal_iso_i - : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)). - admit. - Defined. + Opaque UnderlyingFunctor. + Instance garrow_first a : + (garrow_functor >>>> bin_first(BinoidalCat:=enr_c_bin C) (R' a)) <~~~> + (bin_first(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) := + { ni_iso := fun a => iso_id _ }. + intros. + etransitivity. apply iso_id_lemma1. symmetry. + etransitivity. apply iso_id_lemma2. symmetry. - Lemma garrow_functor_monoidal_iso : - forall X Y:enr_v_mon K, - garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y). - admit. - Defined. + Opaque Underlying. + unfold garrow_functor. + unfold functor_comp at 1. + unfold functor_comp at 1. + Opaque functor_comp. simpl. Transparent functor_comp. + + symmetry. + eapply transitivity. + apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_first (R' a)) f). + unfold functor_comp at 1. + unfold functor_comp at 1. + Opaque functor_comp. simpl. Transparent functor_comp. + + symmetry. + eapply transitivity. + set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq. + unfold functor_comp in qq. + simpl in qq. + apply iso_shift_right' in qq. + apply (fmor_respects(R' >>>> step2_functor) _ _ qq). + + apply (me_faithful(MonicEnrichment:=CMon)). + symmetry. + unfold fmor at 1. + eapply transitivity. + set (ni_commutes (mf_first(PreMonoidalFunctor:=CM) (R' a))) as zz. + unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz. + set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'. + apply iso_shift_right' in zz'. + apply zz'. + + unfold functor_comp; simpl. + + symmetry. + eapply transitivity. + set full_roundtrip as full_roundtrip'. + unfold fmor in full_roundtrip'. + simpl in full_roundtrip'. + apply full_roundtrip'. + + set (@iso_shift_right') as q. simpl in q. apply q. clear q. + + set (@iso_shift_left) as q. simpl in q. apply q. clear q. + + symmetry. + eapply transitivity. + set full_roundtrip as full_roundtrip'. + unfold fmor in full_roundtrip'. + simpl in full_roundtrip'. + apply (fun a' b' f z => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)). + symmetry. + + intros. + unfold bin_obj. + unfold senr_v_bobj. + + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + simpl. + setoid_rewrite <- associativity. + etransitivity. + apply iso_comp1_left. + + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + apply iso_comp1_right. + + eapply symmetry. + eapply transitivity. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + eapply reflexivity. + eapply symmetry. + + eapply transitivity. + apply associativity. + eapply transitivity. + eapply comp_respects; [ reflexivity | idtac ]. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + eapply transitivity. + eapply symmetry. + apply associativity. + apply comp_respects; try apply reflexivity. + + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + eapply associativity. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + apply iso_comp1_left. + + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + eapply comp_respects. + eapply symmetry. + eapply associativity. + eapply reflexivity. + apply iso_comp1_left. - Definition garrow_functor_monoidal_niso - : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + apply associativity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply symmetry. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + eapply transitivity. + eapply transitivity. + apply associativity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply associativity. + eapply transitivity; [ idtac | apply right_identity ]. + eapply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + unfold functor_fobj. + apply fmor_preserves_comp. + setoid_rewrite iso_comp2. + apply fmor_preserves_id. + + apply comp_respects. + reflexivity. + reflexivity. + Defined. + + Instance garrow_second a : + (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a)) + <~~~> (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) := + { ni_iso := fun a => iso_id _ }. admit. Defined. - Opaque homset_tensor_iso. - Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor := - { mf_coherence := garrow_functor_monoidal_niso - ; mf_id := garrow_functor_monoidal_iso_i - }. - admit. - admit. +Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. +Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. +Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. + + Lemma cancell_lemma `(F:PreMonoidalFunctor) b : + iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~ + #((mf_first F b) _) >>> F \ #(pmon_cancell b). + set (mf_cancell(PreMonoidalFunctor:=F) b) as q. + setoid_rewrite associativity in q. + set (@comp_respects) as qq. + unfold Proper in qq. + unfold respectful in qq. + set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'. + setoid_rewrite <- associativity in q'. + clear q qq. + setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'. + eapply transitivity; [ apply q' | idtac ]. + clear q'. + setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + symmetry. + apply iso_shift_left. + setoid_rewrite iso_comp1. + symmetry. + eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))]. + apply (fmor_respects (-⋉ F b)). + apply iso_comp2. + Qed. + + Lemma cancell_coherent (b:enr_v K) : + #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~ + (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>> + #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b). + Opaque Underlying. + Opaque fmor. + intros; simpl. + setoid_rewrite right_identity. + symmetry. + eapply transitivity; [ idtac | apply left_identity ]. + apply comp_respects. + apply (fmor_preserves_id (ebc_first (garrow_functor b))). + unfold garrow_functor. + unfold step2_functor. + Transparent fmor. + unfold functor_fobj. + unfold functor_comp. + simpl. + + apply (me_faithful(MonicEnrichment:=CMon)). + eapply transitivity; [ eapply full_roundtrip | idtac ]. + + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ reflexivity | idtac ]. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ reflexivity | idtac ]. + eapply symmetry. + apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))). + + apply symmetry. + apply iso_shift_left. + + symmetry. + eapply transitivity. + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply symmetry. + set (mf_cancell(PreMonoidalFunctor:=reification) b) as q. + eapply transitivity; [ idtac | apply associativity ]. + apply q. + + apply iso_shift_left'. + eapply transitivity. + apply associativity. + symmetry. + set (@iso_shift_right') as qq. + simpl in qq. + apply qq. + clear qq. + unfold me_homfunctor. + eapply transitivity. + symmetry. + apply (cancell_lemma CM (garrow_fobj b)). + + apply symmetry. + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + eapply symmetry. + eapply associativity. + apply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + apply comp_respects; try reflexivity. + + unfold functor_fobj. + unfold pmon_I. + + set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q. + eapply transitivity. + eapply symmetry. + apply associativity. + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + apply q. + clear q. + unfold fmor; simpl. + + eapply transitivity. + apply associativity. + eapply transitivity; [ idtac | apply right_identity ]. + apply comp_respects; try reflexivity. + apply iso_comp2. + Qed. + + Lemma cancelr_lemma `(F:PreMonoidalFunctor) b : + (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~ + #((mf_first F _) _) >>> F \ #(pmon_cancelr b). + set (mf_cancelr(PreMonoidalFunctor:=F) b) as q. + setoid_rewrite associativity in q. + set (@comp_respects) as qq. + unfold Proper in qq. + unfold respectful in qq. + set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'. + setoid_rewrite <- associativity in q'. + clear q qq. + setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'. + eapply transitivity; [ apply q' | idtac ]. + clear q'. + setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + symmetry. + apply iso_shift_left. + setoid_rewrite iso_comp1. + symmetry. + eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))]. + apply (fmor_respects (-⋉ F b)). + apply iso_comp2. + Qed. + + Lemma cancelr_coherent (b:enr_v K) : + #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~ + (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>> + #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b). + + Opaque Underlying. + Opaque fmor. + intros; simpl. + setoid_rewrite right_identity. + symmetry. + eapply transitivity; [ idtac | apply left_identity ]. + apply comp_respects. + apply (fmor_preserves_id (ebc_second (garrow_functor b))). + unfold garrow_functor. + unfold step2_functor. + Transparent fmor. + unfold functor_fobj. + unfold functor_comp. + simpl. + + apply (me_faithful(MonicEnrichment:=CMon)). + eapply transitivity; [ eapply full_roundtrip | idtac ]. + + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ reflexivity | idtac ]. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)). + + apply symmetry. + apply iso_shift_left. + + symmetry. + eapply transitivity. + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply associativity. + + set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q. + setoid_rewrite associativity in q. + + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + eapply symmetry. + apply associativity. + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + symmetry. + eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + eapply transitivity. + apply associativity. + apply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply comp_respects; [ reflexivity | idtac ]. + apply comp_respects; [ idtac | reflexivity ]. + apply mf_consistent. + eapply symmetry. + apply q. + + apply iso_shift_left'. + eapply transitivity. + apply associativity. + symmetry. + set (@iso_shift_right') as qq. + simpl in qq. + apply qq. + clear qq. + unfold me_homfunctor. + eapply transitivity. + symmetry. + apply (cancelr_lemma CM (garrow_fobj b)). + + unfold functor_fobj. + unfold pmon_I. + + set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q. + apply symmetry. + eapply transitivity. + apply comp_respects; [ idtac | reflexivity ]. + apply comp_respects; [ reflexivity | idtac ]. + eapply symmetry. + apply q. + clear q. + + eapply transitivity. + apply associativity. + apply comp_respects; try reflexivity. + simpl. + + eapply transitivity. + apply associativity. + eapply transitivity; [ idtac | apply right_identity ]. + apply comp_respects; try reflexivity. + apply iso_comp2. + Qed. + + Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor := + { mf_first := garrow_first + ; mf_second := garrow_second + ; mf_i := iso_id _ }. + intros; reflexivity. + intros. + unfold garrow_functor. + unfold fmor. + Opaque fmor. simpl. + unfold step2_functor. + admit. + Transparent fmor. + + apply cancell_coherent. + apply cancelr_coherent. admit. Defined. - Definition garrow_from_reification : GeneralizedArrow K C. - refine - {| ga_functor := garrow_functor - ; ga_functor_monoidal := garrow_functor_monoidal - |}. - Defined. + Definition garrow_from_reification : GeneralizedArrow K CM := + {| ga_functor_monoidal := garrow_monoidal |}. End GArrowFromReification. -Opaque homset_tensor_iso. + diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v index d0d8b84..82bc678 100644 --- a/src/HaskProofFlattener.v +++ b/src/HaskProofFlattener.v @@ -136,7 +136,7 @@ Section HaskProofFlattener. Definition FlatteningFunctor_fmor {Γ}{Δ}{ec} : forall h c, (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) -> - ((obact ec h)~~{TypesL _ _ (SystemFCa _ Γ Δ)}~~>(obact ec c)). + ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)). set (@nil (HaskTyVar Γ ★)) as lev. @@ -162,7 +162,7 @@ Section HaskProofFlattener. (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *) eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. - set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ)) + set (snd_initial(SequentND:=@pl_snd _ _ _ _ (SystemFCa Γ Δ)) (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q. eapply nd_comp. eapply nd_prod. @@ -184,42 +184,45 @@ Section HaskProofFlattener. eapply nd_comp. apply (nd_llecnac ;; nd_prod IHX1 IHX2). clear IHX1 IHX2 X1 X2. - apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))). + (* + apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). + *) + admit. (* nd_cancell becomes RVar;;RuCanL *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. (* nd_cancelr becomes RVar;;RuCanR *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. (* nd_llecnac becomes RVar;;RCanL *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. (* nd_rlecnac becomes RVar;;RCanR *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. (* nd_assoc becomes RVar;;RAssoc *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. (* nd_cossa becomes RVar;;RCossa *) eapply nd_comp; [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ]. - apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). auto. destruct r as [r rp]. @@ -342,7 +345,7 @@ Section HaskProofFlattener. Defined. - Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) := + Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) := { fmor := FlatteningFunctor_fmor }. admit. admit. diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v index d6058e5..1f7d85d 100644 --- a/src/HaskProofStratified.v +++ b/src/HaskProofStratified.v @@ -198,8 +198,6 @@ Section HaskProofStratified. admit. admit. admit. - admit. - admit. Defined. (* @@ -347,31 +345,10 @@ Section HaskProofStratified. admit. admit. admit. - admit. - admit. Defined. Hint Constructors Rule_Flat. - Instance PCF_sequents Γ Δ lev : @SequentCalculus _ (PCFRule Γ Δ lev) _ pcfjudg. - apply Build_SequentCalculus. - intros. - induction a. - destruct a; simpl. - apply nd_rule. - exists (RVar _ _ _ _). - apply PCF_RVar. - apply nd_rule. - exists (RVoid _ _ ). - apply PCF_RVoid. - eapply nd_comp. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply (nd_prod IHa1 IHa2). - apply nd_rule. - exists (RJoin _ _ _ _ _ _). - apply PCF_RJoin. - Defined. - Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z]. admit. Defined. @@ -407,16 +384,30 @@ Section HaskProofStratified. admit. Defined. - Instance PCF_cutrule Γ Δ lev : CutRule (PCF_sequents Γ Δ lev) := - { nd_cut := PCF_cut Γ Δ lev }. - admit. - admit. - admit. - Defined. + Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg := + { snd_cut := PCF_cut Γ Δ lev }. + apply Build_SequentND. + intros. + induction a. + destruct a; simpl. + apply nd_rule. + exists (RVar _ _ _ _). + apply PCF_RVar. + apply nd_rule. + exists (RVoid _ _ ). + apply PCF_RVoid. + eapply nd_comp. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply (nd_prod IHa1 IHa2). + apply nd_rule. + exists (RJoin _ _ _ _ _ _). + apply PCF_RJoin. + admit. + Defined. Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)]. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. + eapply nd_prod; [ apply snd_initial | apply nd_id ]. apply nd_rule. set (@PCF_RJoin Γ Δ lev a b a c) as q'. refine (existT _ _ _). @@ -425,29 +416,38 @@ Section HaskProofStratified. Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)]. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. + eapply nd_prod; [ apply nd_id | apply snd_initial ]. apply nd_rule. set (@PCF_RJoin Γ Δ lev b a c a) as q'. refine (existT _ _ _). apply q'. Defined. - Instance PCF_sequent_join Γ Δ lev : @SequentExpansion _ _ _ _ _ (PCF_sequents Γ Δ lev) (PCF_cutrule Γ Δ lev) := - { se_expand_left := PCF_left Γ Δ lev - ; se_expand_right := PCF_right Γ Δ lev }. + Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ := + { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b + ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }. + admit. admit. admit. admit. admit. + admit. + Defined. + + Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND. + admit. + Defined. + + Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev). + admit. Defined. (* 5.1.3 *) Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) := - { pl_eqv := OrgPCF Γ Δ lev - ; pl_sc := PCF_sequents Γ Δ lev - ; pl_subst := PCF_cutrule Γ Δ lev - ; pl_sequent_join := PCF_sequent_join Γ Δ lev + { pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev + ; pl_snd := PCF_sequents Γ Δ lev }. + (* apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl. apply nd_rule. unfold PCFRule. simpl. @@ -474,26 +474,7 @@ Section HaskProofStratified. exists (RArrange _ _ _ _ _ (RuCanR _)). apply (PCF_RArrange lev _ (a,,[]) _). Defined. - - Instance SystemFCa_sequents Γ Δ : @SequentCalculus _ OrgR _ (mkJudg Γ Δ). - apply Build_SequentCalculus. - intros. - induction a. - destruct a; simpl. - apply nd_rule. - destruct l. - apply org_fc with (r:=RVar _ _ _ _). - auto. - apply nd_rule. - apply org_fc with (r:=RVoid _ _ ). - auto. - eapply nd_comp. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply (nd_prod IHa1 IHa2). - apply nd_rule. - apply org_fc with (r:=RJoin _ _ _ _ _ _). - auto. - Defined. +*) Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ]. intros. @@ -524,16 +505,31 @@ Section HaskProofStratified. apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). Defined. - Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) := - { nd_cut := SystemFCa_cut Γ Δ }. - admit. - admit. - admit. - Defined. + Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) := + { snd_cut := SystemFCa_cut Γ Δ }. + apply Build_SequentND. + intros. + induction a. + destruct a; simpl. + apply nd_rule. + destruct l. + apply org_fc with (r:=RVar _ _ _ _). + auto. + apply nd_rule. + apply org_fc with (r:=RVoid _ _ ). + auto. + eapply nd_comp. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply (nd_prod IHa1 IHa2). + apply nd_rule. + apply org_fc with (r:=RJoin _ _ _ _ _ _). + auto. + admit. + Defined. Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)]. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. + eapply nd_prod; [ apply snd_initial | apply nd_id ]. apply nd_rule. apply org_fc with (r:=RJoin Γ Δ a b a c). auto. @@ -541,12 +537,13 @@ Section HaskProofStratified. Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)]. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. + eapply nd_prod; [ apply nd_id | apply snd_initial ]. apply nd_rule. apply org_fc with (r:=RJoin Γ Δ b a c a). auto. Defined. +(* Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) := { se_expand_left := SystemFCa_left Γ Δ ; se_expand_right := SystemFCa_right Γ Δ }. @@ -555,11 +552,12 @@ Section HaskProofStratified. admit. admit. Defined. - +*) (* 5.1.2 *) - Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR := + Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR. +(* { pl_eqv := OrgNDR - ; pl_sc := SystemFCa_sequents Γ Δ + ; pl_sn := SystemFCa_sequents Γ Δ ; pl_subst := SystemFCa_cutrule Γ Δ ; pl_sequent_join := SystemFCa_sequent_join Γ Δ }. @@ -570,6 +568,8 @@ Section HaskProofStratified. apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR a ))). apply Flat_RArrange. apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a ))). apply Flat_RArrange. apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a ))). apply Flat_RArrange. +*) +admit. Defined. End HaskProofStratified. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index d38286d..06f97a1 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -577,7 +577,7 @@ Section HaskProofToStrong. refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *. + set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *. refine (X_ ξ' (vars,,[vnew]) _ >>>= _). apply FreshMon. simpl. @@ -642,7 +642,7 @@ Section HaskProofToStrong. refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *. + set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 74ecaef..3a06d66 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -137,7 +137,7 @@ Section Natural_Deduction. | nd_id1 : forall h, [ h ] /⋯⋯/ [ h ] (* natural deduction: you may discard conclusions *) - | nd_weak : forall h, [ h ] /⋯⋯/ [ ] + | nd_weak1 : forall h, [ h ] /⋯⋯/ [ ] (* natural deduction: you may duplicate conclusions *) | nd_copy : forall h, h /⋯⋯/ (h,,h) @@ -176,14 +176,13 @@ Section Natural_Deduction. Open Scope nd_scope. Open Scope pf_scope. - (* a proof is "structural" iff it does not contain any invocations of nd_rule *) + (* a predicate on proofs *) + Definition NDPredicate := forall h c, h /⋯⋯/ c -> Prop. + + (* the structural inference rules are those which do not change, add, remove, or re-order the judgments *) Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop := | nd_structural_id0 : Structural nd_id0 | nd_structural_id1 : forall h, Structural (nd_id1 h) - | nd_structural_weak : forall h, Structural (nd_weak h) - | nd_structural_copy : forall h, Structural (nd_copy h) - | nd_structural_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2) - | nd_structural_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2) | nd_structural_cancell : forall {a}, Structural (@nd_cancell a) | nd_structural_cancelr : forall {a}, Structural (@nd_cancelr a) | nd_structural_llecnac : forall {a}, Structural (@nd_llecnac a) @@ -192,6 +191,26 @@ Section Natural_Deduction. | nd_structural_cossa : forall {a b c}, Structural (@nd_cossa a b c) . + (* the closure of an NDPredicate under nd_comp and nd_prod *) + Inductive NDPredicateClosure (P:NDPredicate) : forall {h c}, h /⋯⋯/ c -> Prop := + | ndpc_p : forall h c f, P h c f -> NDPredicateClosure P f + | ndpc_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), + NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1**pf2) + | ndpc_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), + NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1;;pf2). + + (* proofs built up from structural rules via comp and prod *) + Definition StructuralND {h}{c} f := @NDPredicateClosure (@Structural) h c f. + + (* The Predicate (BuiltFrom f P h) asserts that "h" was built from a single occurrence of "f" and proofs which satisfy P *) + Inductive BuiltFrom {h'}{c'}(f:h'/⋯⋯/c')(P:NDPredicate) : forall {h c}, h/⋯⋯/c -> Prop := + | builtfrom_refl : BuiltFrom f P f + | builtfrom_P : forall h c g, @P h c g -> BuiltFrom f P g + | builtfrom_prod1 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f1 ** f2) + | builtfrom_prod2 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f2 ** f1) + | builtfrom_comp1 : forall h x c f1 f2, P h x f1 -> @BuiltFrom _ _ f P x c f2 -> BuiltFrom f P (f1 ;; f2) + | builtfrom_comp2 : forall h x c f1 f2, P x c f1 -> @BuiltFrom _ _ f P h x f2 -> BuiltFrom f P (f2 ;; f1). + (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *) Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl := match sl with @@ -200,30 +219,35 @@ Section Natural_Deduction. | T_Branch a b => nd_prod (nd_id a) (nd_id b) end. - Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] := + Fixpoint nd_weak (sl:Tree ??Judgment) : sl /⋯⋯/ [] := match sl as SL return SL /⋯⋯/ [] with | T_Leaf None => nd_id0 - | T_Leaf (Some x) => nd_weak x - | T_Branch a b => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr + | T_Leaf (Some x) => nd_weak1 x + | T_Branch a b => nd_prod (nd_weak a) (nd_weak b) ;; nd_cancelr end. Hint Constructors Structural. - Lemma nd_id_structural : forall sl, Structural (nd_id sl). + Hint Constructors BuiltFrom. + Hint Constructors NDPredicateClosure. + + Hint Extern 1 => apply nd_structural_id0. + Hint Extern 1 => apply nd_structural_id1. + 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 ndpc_p. + Hint Extern 1 => apply ndpc_prod. + Hint Extern 1 => apply ndpc_comp. + + Lemma nd_id_structural : forall sl, StructuralND (nd_id sl). intros. induction sl; simpl; auto. destruct a; auto. Defined. - Lemma weak'_structural : forall a, Structural (nd_weak' a). - intros. - induction a. - destruct a; auto. - simpl. - auto. - simpl. - auto. - Qed. - (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to * structural variations *) Class ND_Relation := @@ -233,31 +257,31 @@ Section Natural_Deduction. (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *) ; ndr_comp_respects : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c), f === f' -> g === g' -> f;;g === f';;g' ; ndr_comp_associativity : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d), (f;;g);;h === f;;(g;;h) - ; ndr_comp_left_identity : forall `(f:a/⋯⋯/c), nd_id _ ;; f === f - ; ndr_comp_right_identity : forall `(f:a/⋯⋯/c), f ;; nd_id _ === f (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *) ; ndr_prod_respects : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d), f===f' -> g===g' -> f**g === f'**g' ; ndr_prod_associativity : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'), (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa - ; ndr_prod_left_identity : forall `(f:a/⋯⋯/b), (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac - ; ndr_prod_right_identity : forall `(f:a/⋯⋯/b), (f ** nd_id0) === nd_cancelr ;; f ;; nd_rlecnac (* products and composition must distribute over each other *) ; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g') - (* 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 + (* Given a proof f, any two proofs built from it using only structural rules are indistinguishable. Keep in mind that + * nd_weak and nd_copy aren't considered structural, so the hypotheses and conclusions of such proofs will be an identical + * list, differing only in the "parenthesization" and addition or removal of empty leaves. *) + ; ndr_builtfrom_structural : forall `(f:a/⋯⋯/b){a' b'}(g1 g2:a'/⋯⋯/b'), + BuiltFrom f (@StructuralND) g1 -> + BuiltFrom f (@StructuralND) g2 -> + g1 === g2 - ; 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 + (* proofs of nothing are not distinguished from each other *) + ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g - (* 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 + (* 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 - (* any two proofs of nothing are "equally good" *) - ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g + (* duplicating a hypothesis and discarding it is irrelevant *) + ; ndr_copy_then_weak_left : forall a, nd_copy a;; (nd_weak _ ** nd_id _) ;; nd_cancell === nd_id _ + ; ndr_copy_then_weak_right : forall a, nd_copy a;; (nd_id _ ** nd_weak _) ;; nd_cancelr === nd_id _ }. (* @@ -349,74 +373,161 @@ Section Natural_Deduction. end. (* Natural Deduction systems whose judgments happen to be pairs of the same type *) - Section Sequents. - Context {S:Type}. (* type of sequent components *) - Context {sequent:S->S->Judgment}. - Context {ndr:ND_Relation}. + Section SequentND. + Context {S:Type}. (* type of sequent components *) + Context {sequent:S->S->Judgment}. (* pairing operation which forms a sequent from its halves *) Notation "a |= b" := (sequent a b). - Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. - - (* Sequent systems with initial sequents *) - Class SequentCalculus := - { nd_seq_reflexive : forall a, ND [ ] [ a |= a ] - }. - (* Sequent systems with a cut rule *) - Class CutRule (nd_cutrule_seq:SequentCalculus) := - { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] - ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell - ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr - ; nd_cut_associativity : forall {a b c d}, - (nd_id1 (a|=b) ** nd_cut b c d) ;; (nd_cut a b d) === nd_cossa ;; (nd_cut a b c ** nd_id1 (c|=d)) ;; nd_cut a c d + (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *) + Class SequentND := + { snd_initial : forall a, [ ] /⋯⋯/ [ a |= a ] + ; snd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] }. - End Sequents. - - (* Sequent systems in which each side of the sequent is a tree of something *) - Section SequentsOfTrees. - Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}. + Context (sequentND:SequentND). Context (ndr:ND_Relation). - Notation "a |= b" := (sequent a b). - Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. - - (* 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] - }. - Notation "[# a #]" := (nd_rule a) : nd_scope. + (* + * A predicate singling out structural rules, initial sequents, + * and cut rules. + * + * Proofs using only structural rules cannot add or remove + * judgments - their hypothesis and conclusion judgment-trees will + * differ only in "parenthesization" and the presence/absence of + * empty leaves. This means that a proof involving only + * structural rules, cut, and initial sequents can ADD new + * non-empty judgment-leaves only via snd_initial, and can only + * REMOVE non-empty judgment-leaves only via snd_cut. Since the + * initial sequent is a left and right identity for cut, and cut + * is associative, any two proofs (with the same hypotheses and + * conclusions) using only structural rules, cut, and initial + * sequents are logically indistinguishable - their differences + * are logically insignificant. + * + * Note that it is important that nd_weak and nd_copy aren't + * considered to be "structural". + *) + Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop := + | snd_inert_initial : forall a, SequentND_Inert _ _ (snd_initial a) + | snd_inert_cut : forall a b c, SequentND_Inert _ _ (snd_cut a b c) + | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f + . + + (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions + * if those proofs use only initial sequents, cut, and structural rules (see comment above) *) + Class SequentND_Relation := + { sndr_ndr := ndr + ; sndr_inert : forall a b (f g:a/⋯⋯/b), + NDPredicateClosure SequentND_Inert f -> + NDPredicateClosure SequentND_Inert g -> + ndr_eqv f g }. + + End SequentND. + + (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *) + Section ContextND. + Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}. + Context {snd:SequentND(sequent:=sequent)}. + Notation "a |= b" := (sequent a b). - (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *) - Context `{se_cut : @CutRule _ sequent ndr sc}. - Class SequentExpansion := - { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] - ; se_expand_right : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] + (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *) + Class ContextND := + { cnd_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x ] + ; cnd_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x ] + ; cnd_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x ] + ; cnd_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x ] + ; cnd_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x ] + ; cnd_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x ] + ; cnd_expand_left : forall a b c , ND [ a |= b] [ c,,a |= c,,b] + ; cnd_expand_right : forall a b c , ND [ a |= b] [ a,,c |= b,,c] + ; cnd_snd := snd + }. - (* left and right expansion must commute with cut *) - ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; se_expand_left c === nd_seq_reflexive (c,, a) - ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c) - ; se_cut_left : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c) - ; se_cut_right : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c) + Context `(ContextND). + + (* + * A predicate singling out initial sequents, cuts, context expansion, + * and structural rules. + * + * Any two proofs (with the same hypotheses and conclusions) whose + * non-structural rules do nothing other than expand contexts, + * re-arrange contexts, or introduce additional initial-sequent + * conclusions are indistinguishable. One important consequence + * is that asking for a small initial sequent and then expanding + * it using cnd_expand_{right,left} is no different from simply + * asking for the larger initial sequent in the first place. + * + *) + Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop := + | cnd_inert_initial : forall a, ContextND_Inert _ _ (snd_initial a) + | cnd_inert_cut : forall a b c, ContextND_Inert _ _ (snd_cut a b c) + | cnd_inert_structural : forall a b f, Structural f -> ContextND_Inert a b f + | cnd_inert_cnd_ant_assoc : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc x a b c) + | cnd_inert_cnd_ant_cossa : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa x a b c) + | cnd_inert_cnd_ant_cancell : forall x a , ContextND_Inert _ _ (cnd_ant_cancell x a) + | cnd_inert_cnd_ant_cancelr : forall x a , ContextND_Inert _ _ (cnd_ant_cancelr x a) + | cnd_inert_cnd_ant_llecnac : forall x a , ContextND_Inert _ _ (cnd_ant_llecnac x a) + | cnd_inert_cnd_ant_rlecnac : forall x a , ContextND_Inert _ _ (cnd_ant_rlecnac x a) + | cnd_inert_se_expand_left : forall t g s , ContextND_Inert _ _ (@cnd_expand_left _ t g s) + | cnd_inert_se_expand_right : forall t g s , ContextND_Inert _ _ (@cnd_expand_right _ t g s). + + Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} := + { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b), + NDPredicateClosure ContextND_Inert f -> + NDPredicateClosure ContextND_Inert g -> + ndr_eqv f g + ; cndr_sndr := sndr }. - End SequentsOfTrees. + + End ContextND. Close Scope nd_scope. Open Scope pf_scope. End Natural_Deduction. -Coercion nd_cut : CutRule >-> Funclass. +Coercion snd_cut : SequentND >-> Funclass. +Coercion cnd_snd : ContextND >-> SequentND. +Coercion sndr_ndr : SequentND_Relation >-> ND_Relation. +Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation. Implicit Arguments ND [ Judgment ]. Hint Constructors Structural. Hint Extern 1 => apply nd_id_structural. -Hint Extern 1 => apply ndr_structural_indistinguishable. +Hint Extern 1 => apply ndr_builtfrom_structural. +Hint Extern 1 => apply nd_structural_id0. +Hint Extern 1 => apply nd_structural_id1. +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 ndpc_p. +Hint Extern 1 => apply ndpc_prod. +Hint Extern 1 => apply ndpc_comp. +Hint Extern 1 => apply builtfrom_refl. +Hint Extern 1 => apply builtfrom_prod1. +Hint Extern 1 => apply builtfrom_prod2. +Hint Extern 1 => apply builtfrom_comp1. +Hint Extern 1 => apply builtfrom_comp2. +Hint Extern 1 => apply builtfrom_P. + +Hint Extern 1 => apply snd_inert_initial. +Hint Extern 1 => apply snd_inert_cut. +Hint Extern 1 => apply snd_inert_structural. + +Hint Extern 1 => apply cnd_inert_initial. +Hint Extern 1 => apply cnd_inert_cut. +Hint Extern 1 => apply cnd_inert_structural. +Hint Extern 1 => apply cnd_inert_cnd_ant_assoc. +Hint Extern 1 => apply cnd_inert_cnd_ant_cossa. +Hint Extern 1 => apply cnd_inert_cnd_ant_cancell. +Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr. +Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac. +Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac. +Hint Extern 1 => apply cnd_inert_se_expand_left. +Hint Extern 1 => apply cnd_inert_se_expand_right. (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds * of proofs. When only one kind of proof is in use, it's quite helpful though. *) @@ -446,6 +557,21 @@ Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c) intros; apply ndr_prod_respects; auto. Defined. +Section ND_Relation_Facts. + Context `{ND_Relation}. + + (* useful *) + Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f. + intros; apply (ndr_builtfrom_structural f); auto. + Defined. + + (* useful *) + Lemma ndr_comp_left_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (nd_id h ;; f) f. + intros; apply (ndr_builtfrom_structural f); auto. + Defined. + +End ND_Relation_Facts. + (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *) Definition nd_replicate : forall @@ -482,7 +608,7 @@ Definition nd_map with | nd_id0 => let case_nd_id0 := tt in _ | nd_id1 h => let case_nd_id1 := tt in _ - | nd_weak h => let case_nd_weak := tt in _ + | nd_weak1 h => let case_nd_weak := tt in _ | nd_copy h => let case_nd_copy := tt in _ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ @@ -530,7 +656,7 @@ Definition nd_map' with | nd_id0 => let case_nd_id0 := tt in _ | nd_id1 h => let case_nd_id1 := tt in _ - | nd_weak h => let case_nd_weak := tt in _ + | nd_weak1 h => let case_nd_weak := tt in _ | nd_copy h => let case_nd_copy := tt in _ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ @@ -633,7 +759,7 @@ Section ToLatex. rawLatexMath "% nd_id0 " +++ eolL | nd_id1 h' => rawLatexMath indent +++ rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL - | nd_weak h' => rawLatexMath indent +++ + | nd_weak1 h' => rawLatexMath indent +++ rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL | nd_copy h' => rawLatexMath indent +++ rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index fd352e1..7ac59b3 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) (* NaturalDeductionCategory: *) (* *) -(* Natural Deduction proofs form a category (under mild assumptions, see below) *) +(* Natural Deduction proofs form a category *) (* *) (*********************************************************************************************************************************) @@ -48,96 +48,86 @@ Section Judgments_Category. | unfold Symmetric; intros; symmetry; auto | unfold Transitive; intros; transitivity y; auto ]. unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto. - intros; apply ndr_comp_left_identity. - intros; apply ndr_comp_right_identity. + intros; apply (ndr_builtfrom_structural f); auto. + intros; apply (ndr_builtfrom_structural f); auto. intros; apply ndr_comp_associativity. 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. - + (* Judgments form a binoidal category *) 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; simpl; apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *; reflexivity. + intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto. intros; unfold eqv in *; simpl in *. setoid_rewrite <- ndr_prod_preserves_comp. - setoid_rewrite ndr_comp_left_identity. - reflexivity. + apply (ndr_builtfrom_structural (f;;g)); auto. 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; simpl; apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *; reflexivity. + intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto. intros; unfold eqv in *; simpl in *. setoid_rewrite <- ndr_prod_preserves_comp. - setoid_rewrite ndr_comp_left_identity. - reflexivity. + apply (ndr_builtfrom_structural (f;;g)); auto. Defined. Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) := { bin_first := jud_first ; bin_second := jud_second }. + + (* and that category is commutative (all morphisms central) *) + Instance Judgments_Category_Commutative : CommutativeCat Judgments_Category_binoidal. + 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. + + (* Judgments form a premonoidal category *) Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)). - refine - {| iso_forward := nd_assoc - ; iso_backward := nd_cossa |}; - abstract (simpl; auto). + refine {| iso_forward := nd_assoc ; iso_backward := nd_cossa |}. + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto. + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto. Defined. Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a. - refine - {| iso_forward := nd_cancelr - ; iso_backward := nd_rlecnac |}; - abstract (simpl; auto). + refine {| iso_forward := nd_cancelr ; iso_backward := nd_rlecnac |}; + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto. Defined. Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a. - refine - {| iso_forward := nd_cancell - ; iso_backward := nd_llecnac |}; - abstract (simpl; auto). + refine {| iso_forward := nd_cancell ; iso_backward := nd_llecnac |}; + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto. Defined. 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. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. 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. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. 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. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b. intros. apply ni_inv. refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}. - intros; unfold eqv in *; simpl in *. - apply ndr_comp_preserves_assoc. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. 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. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. - Instance Judgments_Category_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] := { pmon_cancelr := jud_mon_cancelr ; pmon_cancell := jud_mon_cancell @@ -146,97 +136,27 @@ Section Judgments_Category. ; pmon_assoc_ll := jud_mon_assoc_ll }. unfold functor_fobj; unfold fmor; simpl; - apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto. - + apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); 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. - + apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto. + intros; unfold eqv; simpl; auto; reflexivity. + intros; unfold eqv; simpl; auto; reflexivity. + intros; unfold eqv; simpl; apply Judgments_Category_Commutative. + intros; unfold eqv; simpl; apply Judgments_Category_Commutative. + intros; unfold eqv; simpl; apply Judgments_Category_Commutative. 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. + (* commutative premonoidal categories are monoidal *) + Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal := + { mon_commutative := Judgments_Category_Commutative }. - 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. - + (* Judgments also happens to have a terminal object - the empty list of judgments *) Instance Judgments_Category_Terminal : TerminalObject Judgments_Category []. - refine {| drop := nd_weak' ; drop_unique := _ |}. + refine {| drop := nd_weak ; drop_unique := _ |}. abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant). Defined. + (* Judgments is also a diagonal category via nd_copy *) Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal. intros. refine {| copy := nd_copy |}; intros; simpl. @@ -260,13 +180,11 @@ Section Judgments_Category. reflexivity. Defined. + (* Judgments is a cartesian category: it has a terminal object, diagonal morphisms, and the right naturalities *) Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal := { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }. - - 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. + intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_left. + intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_right. Defined. End Judgments_Category. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 7831fad..933785a 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -26,6 +26,7 @@ Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import FunctorCategories_ch7_7. +Require Import Enrichments. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. @@ -46,11 +47,11 @@ Section Programming_Language. Open Scope pl_scope. Class ProgrammingLanguage := - { pl_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) - ; pl_tsr :> @TreeStructuralRules Judg Rule T sequent - ; pl_sc :> @SequentCalculus Judg Rule _ sequent - ; pl_subst :> @CutRule Judg Rule _ sequent pl_eqv pl_sc - ; pl_sequent_join :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst + { pl_eqv0 : @ND_Relation Judg Rule + ; pl_snd :> @SequentND Judg Rule _ sequent + ; pl_cnd :> @ContextND Judg Rule T sequent pl_snd + ; pl_eqv1 :> @SequentND_Relation Judg Rule _ sequent pl_snd pl_eqv0 + ; pl_eqv :> @ContextND_Relation Judg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1 }. Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3. @@ -65,15 +66,16 @@ Section Programming_Language. Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. unfold hom; simpl. - apply nd_seq_reflexive. + apply snd_initial. Defined. Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. unfold hom; simpl. - apply pl_subst. + apply snd_cut. Defined. Existing Instance pl_eqv. + Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). refine {| eid := identityProof @@ -81,80 +83,101 @@ Section Programming_Language. |}; intros. 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. - apply nd_cut_right_identity. - unfold identityProof; unfold cutProof; simpl. - symmetry. - apply nd_cut_associativity. + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. Defined. - 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) |}. + Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) := + { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }. intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. - apply se_reflexive_right. + apply (cndr_inert pl_cnd); auto. intros. unfold ehom. unfold comp. simpl. unfold cutProof. - rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (se_expand_right _ c) _ _ (nd_id1 (b|=c0)) - _ (nd_id1 (a,,c |= b,,c)) _ (se_expand_right _ c)). + rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (a,,c |= b,,c)) _ (cnd_expand_right _ _ c)). setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]). setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). - apply se_cut_right. + simpl; eapply cndr_inert. apply pl_eqv. auto. auto. Defined. - 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)))). + Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) := + { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }. intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. - apply se_reflexive_left. + eapply cndr_inert; auto. apply pl_eqv. intros. unfold ehom. unfold comp. simpl. unfold cutProof. - rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (se_expand_left _ c) _ _ (nd_id1 (b|=c0)) - _ (nd_id1 (c,,a |= c,,b)) _ (se_expand_left _ c)). + rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (c,,a |= c,,b)) _ (cnd_expand_left _ _ c)). setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]). setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). - apply se_cut_left. + simpl; eapply cndr_inert. apply pl_eqv. auto. auto. Defined. - Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _). + Definition Types_binoidal : EBinoidalCat TypesL. refine - {| bin_first := Types_first - ; bin_second := Types_second + {| ebc_first := Types_first + ; ebc_second := Types_second |}. Defined. 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 + { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c + ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c }. - admit. - admit. - Defined. + simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + 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. + Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a := + { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a + }. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. 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 + Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a := + { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a }. - admit. - admit. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. + unfold eqv; unfold comp; simpl. + eapply cndr_inert. apply pl_eqv. auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + auto. Defined. - Instance Types_cancelr : Types_first [] <~~~> functor_id _ := - { ni_iso := Types_cancelr_iso }. + 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 }. + intros; unfold eqv; simpl. admit. Defined. - 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. + Instance Types_cancelr : Types_first [] <~~~> functor_id _ := + { ni_iso := Types_cancelr_iso }. + intros; simpl. admit. Defined. @@ -174,35 +197,81 @@ Section Programming_Language. Defined. Instance Types_PreMonoidal : PreMonoidalCat Types_binoidal [] := - { pmon_assoc := Types_assoc - ; pmon_cancell := Types_cancell - ; pmon_cancelr := Types_cancelr - ; pmon_assoc_rr := Types_assoc_rr - ; pmon_assoc_ll := Types_assoc_ll - }. - admit. (* pentagon law *) - admit. (* triangle law *) - intros; simpl; reflexivity. - intros; simpl; reflexivity. - admit. (* assoc central *) - admit. (* cancelr central *) - admit. (* cancell central *) - Defined. + { pmon_assoc := Types_assoc + ; pmon_cancell := Types_cancell + ; pmon_cancelr := Types_cancelr + ; pmon_assoc_rr := Types_assoc_rr + ; pmon_assoc_ll := Types_assoc_ll + }. +(* + apply Build_Pentagon. + intros; simpl. + eapply cndr_inert. apply pl_eqv. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + apply ndpc_prod. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + auto. + auto. + auto. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + apply Build_Triangle; intros; simpl. + eapply cndr_inert. apply pl_eqv. + auto. + apply ndpc_comp. + apply ndpc_comp. + auto. + apply ndpc_comp. + auto. + auto. + auto. + eapply cndr_inert. apply pl_eqv. auto. + auto. +*) +admit. +admit. + intros; simpl; reflexivity. + intros; simpl; reflexivity. + admit. (* assoc central *) + admit. (* cancelr central *) + admit. (* cancell central *) + Defined. - (* Definition TypesEnrichedInJudgments : Enrichment. - refine {| enr_c := TypesL |}. + refine + {| enr_v_mon := Judgments_Category_monoidal _ + ; enr_c_pm := Types_PreMonoidal + ; enr_c_bin := Types_binoidal + |}. Defined. Structure HasProductTypes := { }. - Lemma CartesianEnrMonoidal (e:Enrichment) `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e. + (* + Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment) + `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e. admit. Defined. + *) (* need to prove that if we have cartesian tuples we have cartesian contexts *) + (* Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments. admit. Defined. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index a4f40e3..b613455 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -33,91 +33,6 @@ Require Import FreydCategories. Require Import GeneralizedArrow. -Section ExtendFunctor. - - Context `(F:Functor). - Context (P:c1 -> Prop). - - Definition domain_subcat := FullSubcategory c1 P. - - Definition functor_restricts_to_full_subcat_on_domain_fobj (a:domain_subcat) : c2 := - F (projT1 a). - - Definition functor_restricts_to_full_subcat_on_domain_fmor (a b:domain_subcat)(f:a~~{domain_subcat}~~>b) : - (functor_restricts_to_full_subcat_on_domain_fobj a)~~{c2}~~>(functor_restricts_to_full_subcat_on_domain_fobj b) := - F \ (projT1 f). - - Lemma functor_restricts_to_full_subcat_on_domain : Functor domain_subcat c2 functor_restricts_to_full_subcat_on_domain_fobj. - refine {| fmor := functor_restricts_to_full_subcat_on_domain_fmor |}; - unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros. - setoid_rewrite H; reflexivity. - setoid_rewrite fmor_preserves_id; reflexivity. - setoid_rewrite <- fmor_preserves_comp; reflexivity. - Defined. - -End ExtendFunctor. - -Section MonoidalSubCat. - - (* a monoidal subcategory is a full subcategory, closed under tensor and containing the unit object *) - Class MonoidalSubCat {Ob}{Hom}{C:Category Ob Hom}{MFobj}{MF}{MI}(MC:MonoidalCat C MFobj MF MI) := - { msc_P : MC -> Prop - ; msc_closed_under_tensor : forall o1 o2, msc_P o1 -> msc_P o2 -> msc_P (MC (pair_obj o1 o2)) - ; msc_contains_unit : msc_P (mon_i MC) - ; msc_subcat := FullSubcategory MC msc_P - }. - Local Coercion msc_subcat : MonoidalSubCat >-> SubCategory. - - Context `(MSC:MonoidalSubCat). - - (* any full subcategory of a monoidal category, , is itself monoidal *) - Definition mf_restricts_to_full_subcat_on_domain_fobj (a:MSC ×× MSC) : MSC. - destruct a. - destruct o. - destruct o0. - set (MC (pair_obj x x0)) as m'. - exists m'. - apply msc_closed_under_tensor; auto. - Defined. - - Definition mf_restricts_to_full_subcat_on_domain_fmor - {a}{b} - (f:a~~{MSC ×× MSC}~~>b) - : - (mf_restricts_to_full_subcat_on_domain_fobj a)~~{MSC}~~>(mf_restricts_to_full_subcat_on_domain_fobj b). - destruct a as [[a1 a1pf] [a2 a2pf]]. - destruct b as [[b1 b1pf] [b2 b2pf]]. - destruct f as [[f1 f1pf] [f2 f2pf]]. - simpl in *. - exists (MC \ (pair_mor (pair_obj a1 a2) (pair_obj b1 b2) f1 f2)); auto. - Defined. - - Lemma mf_restricts_to_full_subcat_on_domain : Functor (MSC ×× MSC) MSC - mf_restricts_to_full_subcat_on_domain_fobj. - refine {| fmor := fun a b f => mf_restricts_to_full_subcat_on_domain_fmor f |}; - unfold functor_restricts_to_full_subcat_on_domain_fmor; simpl; intros. - admit. - admit. - admit. - Defined. - - Definition subcat_i : MSC. - exists (mon_i MC). - apply msc_contains_unit. - Defined. - - Lemma full_subcat_is_monoidal : MonoidalCat MSC _ mf_restricts_to_full_subcat_on_domain subcat_i. - admit. - Defined. - - Lemma inclusion_functor_monoidal : MonoidalFunctor full_subcat_is_monoidal MC (InclusionFunctor _ MSC). - admit. - Defined. - -End MonoidalSubCat. -Coercion full_subcat_is_monoidal : MonoidalSubCat >-> MonoidalCat. - -(* Section ArrowInLanguage. (* an Arrow In A Programming Language consists of... *) @@ -133,10 +48,9 @@ Section ArrowInLanguage. (* a premonoidal category enriched in aforementioned full subcategory *) 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). -Check (Underlying KE). + 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 {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}. @@ -153,7 +67,6 @@ Check (Underlying KE). Defined. Context (K_surjective:SurjectiveEnrichment K_enrichment). *) -Check (@FreydCategory). Definition ArrowInProgrammingLanguage := @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K. @@ -163,4 +76,3 @@ Check (@FreydCategory). Defined. End GArrowInLanguage. -*) \ No newline at end of file diff --git a/src/Reification.v b/src/Reification.v index 2b9aac9..932d78e 100644 --- a/src/Reification.v +++ b/src/Reification.v @@ -33,13 +33,13 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := ; reification_rstar_obj : enr_v K -> enr_v C ; reification_r : forall k:K, Functor K C (reification_r_obj k) ; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj -; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f -; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f +; reification_rstar : PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f +; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f }. Transparent HomFunctor. Transparent functor_comp. -Coercion reification_rstar : Reification >-> MonoidalFunctor. +Coercion reification_rstar : Reification >-> PreMonoidalFunctor. Implicit Arguments Reification [ ]. Implicit Arguments reification_r_obj [ K C CI ]. Implicit Arguments reification_r [ K C CI ]. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index e57df4d..9a7c3fd 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -18,13 +18,14 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import WeakFunctorCategory. -Require Import SmallSMMEs. (* * Technically reifications form merely a *semicategory* (no identity @@ -43,8 +44,8 @@ Require Import SmallSMMEs. * use it as a host language. But that's for the next paper... *) Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type := - | roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme - | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1 s2. + | roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme + | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (enr_c_i s2) -> ReificationOrIdentity s1 s2. Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 := match f with @@ -62,30 +63,29 @@ Definition reificationOrIdentityFunc Defined. Definition compose_reifications (s0 s1 s2:SMMEs) : - Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2). + Reification s0 s1 (enr_c_i s1) -> Reification s1 s2 (enr_c_i s2) -> Reification s0 s2 (enr_c_i s2). intros. refine {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0 - ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0) - ; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1)) + ; reification_rstar := PreMonoidalFunctorsCompose (reification_rstar X) (reification_rstar X0) + ; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (enr_c_i s1)) |}. intro K. - set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (HomFunctor s2 (mon_i s2))) as q. + set (ni_associativity (reification_r X K) (reification_r X0 (enr_c_i s1)) (HomFunctor s2 (enr_c_i s2))) as q. eapply ni_comp. apply q. clear q. set (reification_commutes X K) as comm1. - set (reification_commutes X0 (mon_i s1)) as comm2. + set (reification_commutes X0 (enr_c_i s1)) as comm2. set (HomFunctor s0 K) as a in *. set (reification_rstar_f X) as a' in *. set (reification_rstar_f X0) as x in *. set (reification_r X K) as b in *. - set (reification_r X0 (mon_i s1)) as c in *. - set (HomFunctor s2 (mon_i s2)) as c' in *. - set (HomFunctor s1 (mon_i s1)) as b' in *. + set (reification_r X0 (enr_c_i s1)) as c in *. + set (HomFunctor s2 (enr_c_i s2)) as c' in *. + set (HomFunctor s1 (enr_c_i s1)) as b' in *. apply (ni_comp(F2:=b >>>> (b' >>>> x))). - apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)). - apply ni_id. + apply (ni_respects1 b (c >>>> c') (b' >>>> x)). apply comm2. eapply ni_comp. eapply ni_inv. @@ -94,10 +94,9 @@ Definition compose_reifications (s0 s1 s2:SMMEs) : eapply ni_comp. eapply ni_inv. apply (ni_associativity a a' x). - apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x). + apply (ni_respects2 (a >>>> a') (b >>>> b') x). apply ni_inv. apply comm1. - apply ni_id. Defined. Definition reificationOrIdentityComp diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index a53b2e2..2a9937f 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -17,19 +17,21 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C) - : Reification K C (mon_i C). + : Reification K ce (enr_c_i ce). refine - {| reification_r := fun k:K => HomFunctor K k >>>> garrow - ; reification_rstar_f := garrow >>>> me_mf C - ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C) + {| reification_r := fun k:K => HomFunctor K k >>>> ga_functor garrow + ; reification_rstar_f := ga_functor garrow >>>> C + ; reification_rstar := PreMonoidalFunctorsCompose garrow C |}. abstract (intros; set (@ni_associativity) as q; apply q). Defined. diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v index 6a615ac..4056c77 100644 --- a/src/ReificationsAndGeneralizedArrows.v +++ b/src/ReificationsAndGeneralizedArrows.v @@ -19,8 +19,10 @@ Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. +Require Import PreMonoidalCategories. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. +Require Import Enrichments. Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. @@ -35,53 +37,115 @@ Section ReificationsEquivalentToGeneralizedArrows. match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _) end. - Lemma roundtrip_lemma' - `{C:Category}`{D:Category}`{E:Category} - {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) : - ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _). + Lemma roundtrip_lemma + `{D:Category}`{E:Category} + {Gobj}{G:Functor E D Gobj} G_full G_faithful `{C:Category}{Fobj}(F:Functor C (FullImage G) Fobj) : + (F >>>> (ff_functor_section_functor G G_full G_faithful >>>> G)) ≃ (F >>>> FullImage_InclusionFunctor _). + if_transitive. + eapply if_inv. + apply (if_associativity F (ff_functor_section_functor G _ _) G). if_transitive. apply (if_associativity F (ff_functor_section_functor G _ _) G). apply if_respects. apply if_id. if_transitive; [ idtac | apply if_left_identity ]. - apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)). + apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> FullImage_InclusionFunctor _)). apply if_inv. - apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))). + apply (if_associativity (ff_functor_section_functor G G_full G_faithful) + (RestrictToImage G) (FullImage_InclusionFunctor G)). apply if_respects. apply ff_functor_section_splits_niso. apply if_id. Qed. - Definition roundtrip_lemma - `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C)) - := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification). - - Lemma roundtrip_reification_to_reification - `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C)) - : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification). + Definition step1_niso + `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce)) + : reification_rstar reification ≃ (RestrictToImage reification >>>> R' K CM reification >>>> FullImage_InclusionFunctor CM). + exists (fun c1 => homset_tensor_iso K CM reification c1). + intros. simpl. - unfold mon_f. - unfold garrow_functor. - apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))). - apply (@step1_niso _ K _ _ C reification). - apply (if_inv (roundtrip_lemma K C reification)). + etransitivity. + eapply comp_respects; [ apply reflexivity | idtac ]. + apply associativity. + apply iso_comp1_right. Qed. Lemma roundtrip_garrow_to_garrow - `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C) - : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow). - apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)). + `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM) + : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow). + apply if_inv. - apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow) - >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))). - unfold mf_f. + eapply if_comp. + eapply if_inv. unfold garrow_from_reification. + simpl. + unfold mf_F. unfold garrow_functor. - unfold step2_functor. - set (@roundtrip_lemma _ K _ _ C) as q. - apply (q (reification_from_garrow K C garrow)). + apply (if_associativity + (RestrictToImage (reification_from_garrow K CM garrow)) + (R' K CM (reification_from_garrow K CM garrow)) + (step2_functor C)). + + apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative). + eapply if_comp. + apply (if_associativity + (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow)) + (step2_functor C) + me_homfunctor). + + set ((R' K CM (reification_from_garrow K CM garrow))) as f. + unfold HomFunctor_fullimage in f. + set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q. + set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'. + + eapply if_comp. + apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)). + unfold step2_functor. + eapply if_comp. + apply (if_respects + (RestrictToImage (reification_from_garrow K CM garrow)) + (RestrictToImage (reification_from_garrow K CM garrow)) + _ _ (if_id _) q'). + + eapply if_comp. + eapply if_inv. + apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)). + apply if_inv. - apply (step1_niso K C (reification_from_garrow K C garrow)). - Qed. + apply (step1_niso K C CM (reification_from_garrow K CM garrow)). + Qed. + + Lemma roundtrip_reification_to_reification + `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce)) + : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification). + + simpl. + unfold garrow_functor. + + eapply if_comp. + apply (step1_niso K C CM reification). + + unfold garrow_monoidal. + unfold mf_F. + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C) + (HomFunctor ce (pmon_I (enr_c_pm ce)))). + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage reification) (R' K CM reification) + (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))). + + apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)). + apply if_inv. + eapply if_comp. + apply (if_associativity (R' K CM reification) (step2_functor C) (HomFunctor ce _)). + + set ((R' K CM reification)) as f. + unfold HomFunctor_fullimage in f. + set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q. + set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'. + apply q'. + Qed. End ReificationsEquivalentToGeneralizedArrows. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index 8edd1e0..1230454 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -17,9 +17,9 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. -Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. @@ -31,17 +31,17 @@ Require Import ReificationCategory. Require Import ReificationsAndGeneralizedArrows. Require Import WeakFunctorCategory. Require Import BijectionLemma. +Require Import Enrichments. Section ReificationsIsomorphicToGeneralizedArrows. - Definition M1 {c1 c2 : SmallSMMEs.SMMEs} : + Definition M1 {c1 c2 : SMMEs} : (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) -> (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2). intro GA. destruct GA; [ apply roi_id | idtac ]. apply roi_reif. - apply reification_from_garrow. - apply g. + apply (reification_from_garrow s1 s2 g). Defined. (* I tried really hard to avoid this *) @@ -137,18 +137,18 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply if_id. destruct g; simpl. apply if_id. - unfold mf_f; simpl. + simpl. apply (if_associativity - ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))). + ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))). Defined. - Definition M2 (c1 c2 : SmallSMMEs.SMMEs) : + Definition M2 (c1 c2 : SMMEs) : (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) -> (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2). intro RE. destruct RE; [ apply gaoi_id | idtac ]. apply gaoi_ga. - apply (garrow_from_reification s1 s2 r). + apply (garrow_from_reification s1 (smme_mee s2) s2 r). Defined. Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b) @@ -156,38 +156,38 @@ Section ReificationsIsomorphicToGeneralizedArrows. (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') : generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'. unfold hom in *. - set (@roundtrip_garrow_to_garrow _ a _ _ b) as q. + set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon b)) as q. destruct f; simpl in *. apply H. apply if_inv. apply (if_comp (if_inv H)). clear H. - unfold mf_f in q. - apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g)) - (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))). + apply (if_respects + (ga_functor g) + (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g)) + (HomFunctor (senr_c s2) (senr_c_i s2)) + (HomFunctor (senr_c s2) (senr_c_i s2)) + ). apply q. apply if_id. - Qed. - + Qed. Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b) (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b) (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') : reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'. unfold hom in *. - set (@roundtrip_reification_to_reification _ a _ _ b) as q. + set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon b)) as q. destruct f; simpl. apply H. apply if_inv. apply (if_comp (if_inv H)). clear H. simpl. - unfold mf_f; simpl. simpl in q. - unfold mf_f in q. simpl in q. apply q. - Qed. + Qed. Lemma M2_respects : forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b), @@ -198,38 +198,109 @@ Section ReificationsIsomorphicToGeneralizedArrows. unfold eqv in *. simpl in *. destruct f. - set (invert_reif _ f') as q. - destruct q; subst. - apply if_id. - simpl in *. - destruct H0; subst. - simpl in *. - unfold garrow_functor. - unfold step2_functor. - apply (if_comp H). - clear H. - apply (if_comp (@step1_niso _ smme _ _ smme x)). - apply if_inv. - apply (@roundtrip_lemma _ smme _ _ smme x). + set (invert_reif _ f') as q. + destruct q; subst. + apply if_id. + + simpl in *. + destruct H0; subst. + simpl in *. + unfold garrow_functor. + unfold step2_functor. + apply (if_comp H). + clear H. + eapply if_comp. + apply (step1_niso smme (smme_mee smme) (smme_mon smme) x). + apply if_inv. + set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q. + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)). + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>> + ff_functor_section_functor me_homfunctor me_full me_faithful)) + (HomFunctor (senr_c smme) (senr_c_i smme))). + apply (if_respects (RestrictToImage x) (RestrictToImage x)). + apply (if_id (RestrictToImage x)). + unfold mf_F. + unfold me_homfunctor in q. + unfold pmon_I. + apply q. + simpl in *. destruct f'; simpl in *. - apply if_inv. + simpl in *. apply if_inv in H. - apply (if_comp H). + eapply if_comp; [ idtac | eapply if_inv; apply H ]. clear H. unfold garrow_functor. unfold step2_functor. - apply (if_comp (@step1_niso _ smme _ _ smme r)). apply if_inv. - apply (@roundtrip_lemma _ smme _ _ smme r). + eapply if_comp. + apply (step1_niso smme (smme_mee smme) (smme_mon smme) r). + + rename r into x. + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>> + ff_functor_section_functor me_homfunctor me_full me_faithful)) + (HomFunctor (senr_c smme) (senr_c_i smme))). + apply if_inv. + eapply if_comp. + apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)). + apply (if_respects (RestrictToImage x) (RestrictToImage x)). + apply (if_id (RestrictToImage x)). + + unfold mf_F. + set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q. + apply if_inv. + unfold me_homfunctor in q. + unfold pmon_I. + apply q. + simpl in *. unfold garrow_functor. unfold step2_functor. - apply if_inv in H. - apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)). + set (step1_niso s1 (smme_mee s2) s2 r) as q. + apply if_inv in q. + eapply if_comp. + eapply if_comp; [ idtac | apply q ]. + + eapply if_comp. + apply (if_associativity + (RestrictToImage r) + (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) + (HomFunctor (senr_c s2) (senr_c_i s2))). + apply if_inv. + eapply if_comp. + apply (if_associativity + (RestrictToImage r) + (R' s1 s2 r) + (FullImage_InclusionFunctor _)). + apply (if_respects + (RestrictToImage r) + (RestrictToImage r) + (R' s1 s2 r >>>> FullImage_InclusionFunctor _) + (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>> + HomFunctor (senr_c s2) (senr_c_i s2)))). + apply (if_id _). + apply if_inv. + eapply if_comp. + apply (if_associativity + (R' s1 s2 r) + (ff_functor_section_functor me_homfunctor me_full me_faithful) + (HomFunctor (senr_c s2) (senr_c_i s2))). + apply if_inv. + apply (if_respects + (R' s1 s2 r) + (R' s1 s2 r) + (FullImage_InclusionFunctor _) + ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _)) + ). + apply (if_id _). apply if_inv. - apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)). - apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))). + apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))). Qed. Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x). diff --git a/src/SmallSMMEs.v b/src/SmallSMMEs.v deleted file mode 100644 index 828612f..0000000 --- a/src/SmallSMMEs.v +++ /dev/null @@ -1,32 +0,0 @@ -(*********************************************************************************************************************************) -(* SmallSMMEs: *) -(* *) -(* The collection of SMMEs is a collection of small categories (see SmallCategories) *) -(* *) -(*********************************************************************************************************************************) - -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 Enrichment_ch2_8. -Require Import RepresentableStructure_ch7_2. -Require Import GeneralizedArrow. -Require Import WeakFunctorCategory. - - -Definition SMMEs : SmallCategories. - refine {| small_cat := SMME - ; small_cat_cat := fun smme => enr_v smme - |}. - Defined. diff --git a/src/categories b/src/categories index e928451..1104780 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit e928451c4c45cdbdd975bbfb229e8cc2616b8194 +Subproject commit 1104780d775bf36ff9f44ab287c22604ab47f0b5