From f9297f3fba59884fe98eb4f9257a1fb7552bfd0a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 19:12:36 -0700 Subject: [PATCH] use WeakFunctorCategory to prove GArrow/Reification isomorphism --- src/All.v | 3 + src/GeneralizedArrowCategory.v | 63 +++++- src/ReificationCategory.v | 62 +++++- src/ReificationFromGeneralizedArrow.v | 3 +- src/ReificationsEquivalentToGeneralizedArrows.v | 5 - src/ReificationsIsomorphicToGeneralizedArrows.v | 35 ++++ src/SmallSMMEs.v | 32 +++ src/WeakFunctorCategory.v | 244 +++++++++++++++++++++++ 8 files changed, 436 insertions(+), 11 deletions(-) create mode 100644 src/ReificationsIsomorphicToGeneralizedArrows.v create mode 100644 src/SmallSMMEs.v create mode 100644 src/WeakFunctorCategory.v diff --git a/src/All.v b/src/All.v index 52bfa4a..f5e5157 100644 --- a/src/All.v +++ b/src/All.v @@ -72,9 +72,12 @@ Require Import Reification. Require Import GeneralizedArrow. Require Import GeneralizedArrowFromReification. Require Import ReificationFromGeneralizedArrow. +Require Import WeakFunctorCategory. +Require Import SmallSMMEs. Require Import ReificationCategory. Require Import GeneralizedArrowCategory. Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import ReificationsIsomorphicToGeneralizedArrows. Require Import HaskProofCategory. Require Import ProgrammingLanguage. diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index 974fdc3..a9bedbb 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -23,7 +23,64 @@ Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import GeneralizedArrow. +Require Import WeakFunctorCategory. +Require Import SmallSMMEs. -Definition CategoryOfGeneralizedArrows : Category SMME (fun x y => @GeneralizedArrow x _ y). - admit. - Qed. +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 compose_generalizedArrows (s0 s1 s2:SMMEs) : + GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2. + intro g01. + intro g12. + refine + {| ga_functor := g01 >>>> RepresentableFunctor s1 (mon_i s1) >>>> g12 |}. + apply MonoidalFunctorsCompose. + apply MonoidalFunctorsCompose. + apply (ga_functor_monoidal g01). + apply (me_mf s1). + apply (ga_functor_monoidal g12). + Defined. + +Definition generalizedArrowOrIdentityComp + : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3. + intros. + destruct X. + apply X0. + destruct X0. + apply (gaoi_ga _ _ g). + apply (gaoi_ga _ _ (compose_generalizedArrows _ _ _ g g0)). + Defined. + +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_comp := generalizedArrowOrIdentityComp + |}; intros; simpl. + apply if_id. + destruct f as [|fobj f]; simpl in *. + apply if_inv. + apply if_left_identity. + destruct g as [|gobj g]; simpl in *. + apply if_inv. + apply if_right_identity. + unfold mf_F. + idtac. + unfold mf_f. + apply if_associativity. + Defined. + +Definition CategoryOfGeneralizedArrows := + WeakFunctorCategory MorphismsOfCategoryOfGeneralizedArrows. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index d271c02..b4d444a 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -23,7 +23,65 @@ Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import Reification. +Require Import WeakFunctorCategory. +Require Import SmallSMMEs. -Definition CategoryOfReifications : Category SMME (fun x y:SMME => Reification (smme_e x) (smme_e y) (mon_i (smme_mon y))). +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. + +Definition reificationOrIdentityFunc + : forall s1 s2, ReificationOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }. + intros. + destruct X. + exists (fun x => x). + apply functor_id. + exists (reification_rstar_obj r). + apply r. + 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). + intros. + refine + {| 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. + set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (RepresentableFunctor s2 (mon_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. admit. - Qed. \ No newline at end of file + Defined. + +Definition reificationOrIdentityComp + : forall s1 s2 s3, ReificationOrIdentity s1 s2 -> ReificationOrIdentity s2 s3 -> ReificationOrIdentity s1 s3. + intros. + destruct X. + apply X0. + destruct X0. + apply (roi_reif _ _ r). + apply (roi_reif _ _ (compose_reifications _ _ _ r r0)). + Defined. + +Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs. + refine {| small_func := ReificationOrIdentity + ; small_func_id := fun s => roi_id s + ; small_func_func := fun smme1 smme2 f => projT2 (reificationOrIdentityFunc _ _ f) + ; small_func_comp := reificationOrIdentityComp + |}; intros; simpl. + apply if_id. + destruct f as [|fobj f]; simpl in *. + apply if_inv. + apply if_left_identity. + destruct g as [|gobj g]; simpl in *. + apply if_inv. + apply if_right_identity. + apply if_id. + Defined. + +Definition CategoryOfReifications := + WeakFunctorCategory MorphismsOfCategoryOfReifications. diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index 8d94dca..e6f8ad6 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -29,9 +29,10 @@ Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) refine {| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow ; reification_rstar_f := garrow >>>> me_mf C + ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C) |}. - apply MonoidalFunctorsCompose. abstract (intros; set (@ni_associativity) as q; apply q). Defined. + diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v index bb5df17..0428638 100644 --- a/src/ReificationsEquivalentToGeneralizedArrows.v +++ b/src/ReificationsEquivalentToGeneralizedArrows.v @@ -83,9 +83,4 @@ Section ReificationsEquivalentToGeneralizedArrows. apply (step1_niso K C (reification_from_garrow K C garrow)). Qed. - (* - Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows. - admit. - Qed.*) - End ReificationsEquivalentToGeneralizedArrows. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v new file mode 100644 index 0000000..db11897 --- /dev/null +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -0,0 +1,35 @@ +(*********************************************************************************************************************************) +(* ReificationsEquivalentToGeneralizedArrows: *) +(* *) +(* The category of generalized arrows and the category of reifications are equivalent categories. *) +(* *) +(*********************************************************************************************************************************) + +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 Reification. +Require Import GeneralizedArrow. +Require Import GeneralizedArrowFromReification. +Require Import ReificationFromGeneralizedArrow. +Require Import ReificationCategory. +Require Import GeneralizedArrowCategory. +Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import WeakFunctorCategory. + +Section ReificationsIsomorphicToGeneralizedArrows. + +End ReificationsIsomorphicToGeneralizedArrows. diff --git a/src/SmallSMMEs.v b/src/SmallSMMEs.v new file mode 100644 index 0000000..828612f --- /dev/null +++ b/src/SmallSMMEs.v @@ -0,0 +1,32 @@ +(*********************************************************************************************************************************) +(* 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/WeakFunctorCategory.v b/src/WeakFunctorCategory.v new file mode 100644 index 0000000..49a5189 --- /dev/null +++ b/src/WeakFunctorCategory.v @@ -0,0 +1,244 @@ +(*********************************************************************************************************************************) +(* WeakFunctorCategory: *) +(* *) +(* A category whose morphisms are functors, identified up to natural isomorphism (not equality). This pulls most of the *) +(* heavy lifting out of ReificationsEquivalentToGeneralizedArrows, since the definitions in that context cause Coq to bog *) +(* down and run unbearably slowly *) +(* *) +(*********************************************************************************************************************************) + +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.*) + +Section WeakFunctorCategory. + + (* We can't handle categories directly due to size issues. + * Therefore, we ask the user to supply two types "Cat" and "Mor" + * which index the "small categories"; we then construct a large + * category relative to those. *) + Structure SmallCategories := + { small_cat : Type + ; small_ob : small_cat -> Type + ; small_hom : forall c:small_cat, small_ob c -> small_ob c -> Type + ; small_cat_cat : forall c:small_cat, Category (small_ob c) (small_hom c) + }. + + Context {sc:SmallCategories}. + Structure SmallFunctors := + { small_func : small_cat sc -> small_cat sc -> Type + ; small_func_fobj : forall {c1}{c2}, small_func c1 c2 -> (small_ob sc c1 -> small_ob sc c2) + ; small_func_func : forall {c1}{c2}(f:small_func c1 c2), Functor (small_cat_cat sc c1) (small_cat_cat sc c2) (small_func_fobj f) + + (* proof that our chosen indexing contains identity functors and is closed under composition *) + ; small_func_id : forall c1 , small_func c1 c1 + ; small_func_id_id : forall {c1}, small_func_func (small_func_id c1) ≃ functor_id (small_cat_cat sc c1) + ; small_func_comp : forall {c1}{c2}{c3}, small_func c1 c2 -> small_func c2 c3 -> small_func c1 c3 + ; small_func_comp_comp : forall {c1}{c2}{c3}(f:small_func c1 c2)(g:small_func c2 c3), + small_func_func (small_func_comp f g) ≃ small_func_func f >>>> small_func_func g + }. + + Instance WeakFunctorCategory `(sf:SmallFunctors) : Category (small_cat sc) (small_func sf) := + { id := fun a => small_func_id sf a + ; comp := fun a b c f g => small_func_comp sf f g + ; eqv := fun a b f g => small_func_func sf f ≃ small_func_func sf g + }. + intros; simpl. + apply Build_Equivalence. + unfold Reflexive; simpl; intros; apply if_id. + unfold Symmetric; simpl; intros; apply if_inv; auto. + unfold Transitive; simpl; intros; eapply if_comp. apply H. apply H0. + intros; simpl. + unfold Proper; unfold respectful; simpl; intros. + eapply if_comp. + apply small_func_comp_comp. + eapply if_inv. + eapply if_comp. + apply small_func_comp_comp. + eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0. + intros; simpl. + eapply if_comp. + apply small_func_comp_comp. + eapply if_comp; [ idtac | apply if_left_identity ]. + eapply if_respects; try apply if_id. + apply small_func_id_id. + intros; simpl. + eapply if_comp. + apply small_func_comp_comp. + eapply if_comp; [ idtac | apply if_right_identity ]. + eapply if_respects; try apply if_id. + apply small_func_id_id. + intros; simpl. + eapply if_comp. + eapply if_comp ; [ idtac | apply small_func_comp_comp ]. + apply if_id. + apply if_inv. + eapply if_comp. + eapply if_comp ; [ idtac | apply small_func_comp_comp ]. + apply if_id. + eapply if_comp. + eapply if_respects. + eapply if_id. + eapply small_func_comp_comp. + apply if_inv. + eapply if_comp. + eapply if_respects. + eapply small_func_comp_comp. + eapply if_id. + set (@if_associativity) as q. + apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)). + Defined. +End WeakFunctorCategory. +Coercion WeakFunctorCategory : SmallFunctors >-> Category. +Coercion small_func_func : small_func >-> Functor. +Coercion small_cat_cat : small_cat >-> Category. +Coercion small_cat : SmallCategories >-> Sortclass. + +(* +Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b) + reflexivity proved by (@Equivalence_Reflexive _ _ (eqv_equivalence a b)) + symmetry proved by (@Equivalence_Symmetric _ _ (eqv_equivalence a b)) + transitivity proved by (@Equivalence_Transitive _ _ (eqv_equivalence a b)) + as parametric_relation_eqv. + Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c) + with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp. + auto. + Defined.*) + +Section WeakFunctorCategoryIsomorphism. + (* Here we sort of set up exactly the conditions needed to trigger + * the ReificationsAreGeneralizedArrows proof; again, I'm doing it here + * because the instant I import Reification or GeneralizedArrow, Coq + * becomes nearly unusable. *) + + (* same objects (SMME's) for both categories, and the functor is IIO *) + Context {SMMEs:SmallCategories}. + Context {GA:@SmallFunctors SMMEs}. + Context {RE:@SmallFunctors SMMEs}. + + Context (M1:forall c1 c2, (c1~~{GA}~~>c2) -> (c1~~{RE}~~>c2)). + Context (M2:forall c1 c2, (c1~~{RE}~~>c2) -> (c1~~{GA}~~>c2)). + Implicit Arguments M1 [[c1][c2]]. + Implicit Arguments M2 [[c1][c2]]. + + Section GeneralCase. + Context (m1_respects_eqv + : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2) (g:c1~~{GA}~~>c2), + (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func RE (M1 f) ≃ small_func_func RE (M1 g)). + Context (m2_respects_eqv + : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2) (g:c1~~{RE}~~>c2), + (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func GA (M2 f) ≃ small_func_func GA (M2 g)). + Context (m1_preserves_id + : forall c1, small_func_func _ (M1 (small_func_id GA c1)) ≃ small_func_id RE c1). + Context (m2_preserves_id + : forall c1, small_func_func _ (M2 (small_func_id RE c1)) ≃ small_func_id GA c1). + Context (m1_respects_comp : + forall (c1 c2 c3:SMMEs) (f:c1~~{GA}~~>c2) (g:c2~~{GA}~~>c3), + small_func_func _ (small_func_comp _ (M1 f) (M1 g)) ≃ + small_func_func _ ((M1 (small_func_comp _ f g)))). + Context (m2_respects_comp : + forall (c1 c2 c3:SMMEs) (f:c1~~{RE}~~>c2) (g:c2~~{RE}~~>c3), + small_func_func _ (small_func_comp _ (M2 f) (M2 g)) ≃ + small_func_func _ ((M2 (small_func_comp _ f g)))). + Context (m1_m2_id + : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2), + small_func_func _ (M2 (M1 f)) ≃ small_func_func _ f). + Context (m2_m1_id + : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2), + small_func_func _ (M1 (M2 f)) ≃ small_func_func _ f). + + Definition F1 : Functor GA RE (fun x => x). + refine {| fmor := fun a b f => M1 f |}. + intros. + unfold eqv; simpl. + apply m1_respects_eqv. + apply H. + intros. + unfold eqv; simpl; intros. + apply m1_preserves_id. + intros. + unfold eqv; simpl. + set m1_respects_comp as q. + unfold eqv in q. + apply q. + Defined. + + Definition F2 : Functor RE GA (fun x => x). + refine {| fmor := fun a b f => M2 f |}. + intros. + unfold eqv; simpl. + apply m2_respects_eqv. + apply H. + intros. + unfold eqv; simpl; intros. + apply m2_preserves_id. + intros. + unfold eqv; simpl. + set m2_respects_comp as q. + unfold eqv in q. + apply q. + Defined. + + Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2. + apply Build_IsomorphicCategories. + unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. + eapply if_comp. + apply m1_m2_id. + apply H. + unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. + eapply if_comp. + apply m2_m1_id. + apply H. + Qed. + + End GeneralCase. +(* + (* now, the special case we can really use: M1 and M2 each consist of post-composition *) + Section WeakFunctorCategoryPostCompositionIsomorphism. + + Context (M1_postcompose_obj : forall c1:SMMEs, c1 -> c1). + Context (M1_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)). + + Context (M2_postcompose_obj : forall c1:SMMEs, c1 -> c1). + Context (M2_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)). + + Context (M1_M2_id : forall c1:SMMEs, M1_postcompose c1 >>>> M2_postcompose c1 ≃ functor_id _). + Context (M2_M1_id : forall c1:SMMEs, M2_postcompose c1 >>>> M1_postcompose c1 ≃ functor_id _). + + Context (M1_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{GA}~~>c2), + small_func_func _ (M1 f) ≃ small_func_func _ f >>>> M1_postcompose c2). + Context (M2_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{RE}~~>c2), + small_func_func _ (M2 f) ≃ small_func_func _ f >>>> M2_postcompose c2). + + Definition F1' : Functor GA RE (fun x => x). + apply F1; intros; simpl. + eapply if_comp. + apply M1_postcompose_act. + apply if_inv. + eapply if_comp. + apply M1_postcompose_act. + apply if_respects; try apply if_id. + apply if_inv; auto. + apply (if_comp (M1_postcompose_act _ _ _)). + apply M1_postcompose_act. + + + Theorem WeakFunctorCategoryPostCompositionIsomorphism : IsomorphicCategories GA RE F1 F2 + End WeakFunctorCategoryPostCompositionIsomorphism. + *) +End WeakFunctorCategoryIsomorphism. + + -- 1.7.10.4