From: Adam Megacz Date: Sun, 27 Mar 2011 19:27:50 +0000 (-0700) Subject: almost finished with main theorem X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=d2526b193694dd7a5c7ab9d80d6b6656a7459bb9;hp=165690fe34fc2c88efa57cd2212db1ee324c4385 almost finished with main theorem --- diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index a9bedbb..3ec6660 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -26,19 +26,36 @@ Require Import GeneralizedArrow. Require Import WeakFunctorCategory. Require Import SmallSMMEs. +(* + * Technically reifications form merely a *semicategory* (no identity + * maps), but one can always freely adjoin identity maps (and nothing + * else) to a semicategory to get a category whose non-identity-map + * portion is identical to the original semicategory + * + * Also, technically this category has ALL enrichments (not just the + * surjective monic monoidal ones), though there maps OUT OF only the + * surjective enrichments and INTO only the monic monoidal + * enrichments. It's a big pain to do this in Coq, but sort of might + * matter in real life: a language with really severe substructural + * restrictions might fail to be monoidally enriched, meaning we can't + * use it as a host language. But that's for the next paper... + *) Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type := | gaoi_id : forall smme:SMMEs, GeneralizedArrowOrIdentity smme smme | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2 -> GeneralizedArrowOrIdentity s1 s2. -Definition generalizedArrowOrIdentityFunc - : forall s1 s2, GeneralizedArrowOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }. - intros. - destruct X. - exists (fun x => x). - apply functor_id. - eapply existT. - apply (g >>>> RepresentableFunctor s2 (mon_i s2)). - Defined. +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) + 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 >>>> RepresentableFunctor s2 (mon_i s2) + end. Definition compose_generalizedArrows (s0 s1 s2:SMMEs) : GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2. @@ -66,7 +83,7 @@ Definition generalizedArrowOrIdentityComp Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs. refine {| small_func := GeneralizedArrowOrIdentity ; small_func_id := fun s => gaoi_id s - ; small_func_func := fun smme1 smme2 f => projT2 (generalizedArrowOrIdentityFunc _ _ f) + ; small_func_func := fun smme1 smme2 f => generalizedArrowOrIdentityFunc _ _ f ; small_func_comp := generalizedArrowOrIdentityComp |}; intros; simpl. apply if_id. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index f17caa5..627aa22 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -107,14 +107,6 @@ Section GArrowFromReification. apply (fmor_preserves_comp reification)). Defined. -(* - Definition FullImage_Monoidal - `(F:@Functor Cobj CHom C1 Dobj DHom D1 Fobj) `(mc:MonoidalCat D1 Mobj MF) : MonoidalCat (FullImage F) Mobj. - - Definition step1_functor_monoidal : MonoidalFunctor (enr_v_mon K) step1_functor. - admit. - Defined. -*) Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))). exists (fun c1 => homset_tensor_iso c1). abstract (intros; @@ -130,15 +122,30 @@ Section GArrowFromReification. Definition garrow_functor := step1_functor >>>> step2_functor. - Definition garrow_from_reification : GeneralizedArrow K C. - refine {| ga_functor := garrow_functor |}. - (* - unfold garrow_functor. - apply MonoidalFunctorsCompose. - apply MonoidalFunctorsCompose. - *) + Lemma garrow_functor_monoidal_niso + : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor. + admit. + Defined. + Lemma garrow_functor_monoidal_iso + : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)). + admit. + Defined. + + Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor := + { mf_coherence := garrow_functor_monoidal_niso + ; mf_id := garrow_functor_monoidal_iso + }. + admit. + admit. admit. Defined. + Definition garrow_from_reification : GeneralizedArrow K C. + refine + {| ga_functor := garrow_functor + ; ga_functor_monoidal := garrow_functor_monoidal + |}. + Defined. + End GArrowFromReification. Opaque homset_tensor_iso. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index f735679..0227f60 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -26,6 +26,19 @@ Require Import Reification. Require Import WeakFunctorCategory. Require Import SmallSMMEs. +(* Technically reifications form merely a *semicategory* (no identity + * maps), but one can always freely adjoin identity maps (and nothing + * else) to a semicategory to get a category whose non-identity-map + * portion is identical to the original semicategory + * + * Also, technically this category has ALL enrichments (not just the + * surjective monic monoidal ones), though there maps OUT OF only the + * surjective enrichments and INTO only the monic monoidal + * enrichments. It's a big pain to do this in Coq, but sort of might + * matter in real life: a language with really severe substructural + * restrictions might fail to be monoidally enriched, meaning we can't + * 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. @@ -49,7 +62,8 @@ 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). intros. refine - {| reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0) + {| 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)) |}. intro K. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index dc2f6b0..5163c26 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -30,10 +30,9 @@ Require Import GeneralizedArrowCategory. Require Import ReificationsEquivalentToGeneralizedArrows. Require Import WeakFunctorCategory. - Section ReificationsIsomorphicToGeneralizedArrows. - Definition M1 (c1 c2 : SmallSMMEs.SMMEs) : + Definition M1 {c1 c2 : SmallSMMEs.SMMEs} : (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) -> (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2). intro GA. @@ -43,6 +42,48 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply g. Defined. + Lemma invert_ga : forall (a: SMME) + (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a), + (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f'). + admit. + Qed. + + Lemma invert_reif : forall (a: SMME) + (f:a~~{MorphismsOfCategoryOfReifications}~~>a), + (f = roi_id _) \/ (exists f', f = roi_reif _ _ f'). + admit. + Qed. + + Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x). + refine {| fmor := fun a b f => M1 f |}. + intros. + unfold hom in *. + unfold eqv in *. + simpl in *. + destruct f. + set (invert_ga _ f') as q. + destruct q; subst. + apply if_id. + simpl in *. + destruct H0; subst. + apply H. + simpl in *. + destruct f'; simpl in *. + apply H. + apply H. + intros; simpl. + apply if_id. + intros. + simpl. + destruct f; simpl. + apply if_id. + destruct g; simpl. + apply if_id. + unfold mf_f; simpl. + apply (if_associativity + ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))). + Defined. + Definition M2 (c1 c2 : SmallSMMEs.SMMEs) : (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) -> (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2). @@ -52,35 +93,101 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply (garrow_from_reification s1 s2 r). Defined. - (* + Lemma M2_respects : + forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b), + f ~~ f' -> + M2 a b f ~~ M2 a b f'. + intros. + unfold hom in *. + 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). + simpl in *. + destruct f'; simpl in *. + apply if_inv. + apply if_inv in H. + apply (if_comp 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). + simpl in *. + unfold garrow_functor. + unfold step2_functor. + apply if_inv in H. + set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy. + set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'. + apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)). + apply if_inv. + apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)). + apply yy'. + Qed. - * Oh my, this is massively embarrassing. In the paper I claim - * that Generalized Arrows form a category and Reifications form a - * category, when in fact they form merely a SEMIcategory (see - * http://ncatlab.org/nlab/show/semicategory) since we cannot be sure that the identity functor on the + Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x). + refine {| fmor := fun a b f => M2 _ _ f |}. + apply M2_respects. + intros; simpl; apply if_id. + intros. + simpl. + destruct f; simpl. + apply if_id. + destruct g; simpl. + apply if_id. + unfold mf_f; simpl. + apply (if_respects + (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0)) + (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0))) + (G0:=(RepresentableFunctor s2 (mon_i s2))) + (G1:=(RepresentableFunctor s2 (mon_i s2)))); + [ idtac | apply if_id ]. + admit. + Defined. Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications. - apply WeakFunctorCategoriesIsomorphic with (M1:=M1) (M2:=M2). - destruct g. - intros. - simpl. - simpl in H. - split f. - destruct f. - dependent destruction f. - intros until g. - destruct f. - simpl. - inversion g. - destruct f as [ ] _eqn. - destruct g as [ ] _eqn. - destruct g. - subst. - simpl. - case g. - simpl. - inversion g; subst; intros. - destruct g. - Qed. + refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}. + unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. + unfold hom in *. + set (@roundtrip_garrow_to_garrow _ a _ _ 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:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))). + apply q. + apply if_id. + + unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. + unfold hom in *. + set (@roundtrip_reification_to_reification _ a _ _ 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. End ReificationsIsomorphicToGeneralizedArrows.