X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsIsomorphicToGeneralizedArrows.v;h=5163c2680917a385dd58789c3ac01b8adbb603f7;hp=dc2f6b0f39a09611b25869d6329a011dca8e62ad;hb=d2526b193694dd7a5c7ab9d80d6b6656a7459bb9;hpb=e536cc4194f350ed6de5d465bcf53fda650b3d12 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.