X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsIsomorphicToGeneralizedArrows.v;h=12304542a1f610d3d87be536d195ff27c9139add;hp=756d250a2c8354122fbd744fa88d5ef34d770018;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hpb=e16cc65abd44b09ad0193ff59dd4cd24e4840d0d diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index 756d250..1230454 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) -(* ReificationsEquivalentToGeneralizedArrows: *) +(* ReificationsIsomorphicToGeneralizedArrows: *) (* *) -(* The category of generalized arrows and the category of reifications are equivalent categories. *) +(* The category of generalized arrows and the category of reifications are isomorphic categories. *) (* *) (*********************************************************************************************************************************) @@ -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. @@ -27,43 +27,21 @@ Require Import GeneralizedArrowFromReification. Require Import ReificationFromGeneralizedArrow. Require Import ReificationCategory. Require Import GeneralizedArrowCategory. -Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import ReificationCategory. +Require Import ReificationsAndGeneralizedArrows. Require Import WeakFunctorCategory. +Require Import BijectionLemma. +Require Import Enrichments. Section ReificationsIsomorphicToGeneralizedArrows. - (* - Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) : - ∀A : enr_v_mon s0, - garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A)) - ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A. - *) - - Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) : - (step1_functor s0 s1 r01 >>>> - InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12 - ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12). - unfold IsomorphicFunctors. - simpl. - idtac. - unfold compose_reifications at 0. - eapply Build_IsomorphicFunctors. - unfold step1_functor. - unfold InclusionFunctor. - simpl. - unfold functor_comp. - simpl. - admit. - Defined. - - 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 *) @@ -159,20 +137,58 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply if_id. destruct g; simpl. apply if_id. - unfold mf_f; simpl. + simpl. apply (if_associativity - ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor 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) + (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b) + (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 (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. + 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. + + 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 (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. + simpl in q. + simpl in q. + apply q. + Qed. + Lemma M2_respects : forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b), f ~~ f' -> @@ -182,119 +198,131 @@ 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. - 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)). + 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 yy'. + apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))). Qed. 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 ]. - eapply if_comp. - idtac. - apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)). - Set Printing Coercions. - idtac. - unfold garrow_functor at 1. - unfold step2_functor at 1. - set (roundtrip_lemma' - (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0))) - (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0)) - (step1_functor (smme_see s1) (smme_mee s0) r) - ) as q. - set (if_respects - (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0) - (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0) - q (if_id _)) as q'. - apply (if_comp q'). - Unset Printing Coercions. - clear q' q. - unfold garrow_functor at 2. - unfold garrow_functor at 1. - eapply if_comp. - eapply if_inv. - apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)). - apply (if_respects - (G0:=step2_functor s2) - (G1:=step2_functor s2)); [ idtac | apply if_id ]. - apply step1_lemma. - Defined. + intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros. + apply M2_respects; auto. + unfold fmor; simpl. + apply (@eqv1 _ _ f0 f0). + apply if_id. + unfold fmor; simpl. + apply (@eqv2 _ _ f0 f0). + apply if_id. + Defined. Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications. 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. - + apply (eqv1 _ _ f f'); auto. 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. + apply (eqv2 _ _ f f'); auto. + Qed. End ReificationsIsomorphicToGeneralizedArrows.