X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsIsomorphicToGeneralizedArrows.v;h=b95f30f8078fbdadd9c5b0d567fb0248ba6543f0;hp=db118978baff38690e47c6608fe57da5f11d3c4d;hb=d69d4c8660d8f1f3ea13868c2e2d1c7f8a4d68f7;hpb=f9297f3fba59884fe98eb4f9257a1fb7552bfd0a

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index db11897..b95f30f 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,9 +27,341 @@ 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.
 
+    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 s1 s2 g).
+      Defined.
+
+    (* I tried really hard to avoid this *)
+    Require Import Coq.Logic.Eqdep.
+
+    Inductive Heq : forall {A}{B}, A -> B -> Prop :=
+      heq : forall {A} (a:A), Heq a a.
+
+    Lemma invert_ga' : forall (a b: SMME)
+      (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
+      (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
+      intros.
+      destruct f.
+      left; apply heq.
+      subst; right.
+      exists g.
+      apply heq.
+      Defined.
+
+    Lemma invert_ga : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
+      (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
+      intros.
+      set (invert_ga' a a f (refl_equal a)) as q.
+      destruct q.
+      left.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      right.
+      destruct H.
+      exists x.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      Qed.
+
+    Lemma invert_reif' : forall (a b: SMME)
+      (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
+      (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
+      intros.
+      destruct f.
+      left; apply heq.
+      subst; right.
+      exists r.
+      apply heq.
+      Defined.
+
+    Lemma invert_reif : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
+      (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
+      intros.
+      set (invert_reif' a a f (refl_equal a)) as q.
+      destruct q.
+      left.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      right.
+      destruct H.
+      exists x.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      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.
+        simpl.
+        apply (if_associativity 
+          ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
+        Defined.
+
+    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 (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' ->
+         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.
+          eapply if_comp.
+          apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
+          apply if_inv.
+          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.
+          eapply if_comp.
+            apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+              (HomFunctor (senr_c smme) (senr_c_i smme))).
+          set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+          set (R' smme smme x) as f.
+          set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+          unfold HomFunctor_fullimage in f.
+          unfold mf_F in f.
+          set (q ff _ _ (FullImage x) _ f) as q'.
+          unfold me_homfunctor in q'.
+          exact q'.
+
+      simpl in *.
+        destruct f'; simpl in *.
+        simpl in *.
+        apply if_inv in H.
+        eapply if_comp; [ idtac | eapply if_inv; apply H ].
+        clear H.
+        unfold garrow_functor.
+        unfold step2_functor.
+        apply if_inv.
+        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.
+        apply if_inv.
+
+        eapply if_comp.
+          apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+            (HomFunctor (senr_c smme) (senr_c_i smme))).
+        set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+          set (R' smme smme x) as f.
+          set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+          unfold HomFunctor_fullimage in f.
+          unfold mf_F in f.
+          set (q ff _ _ (FullImage x) _ f) as q'.
+          unfold me_homfunctor in q'.
+          exact q'.
+
+      simpl in *.
+        unfold garrow_functor.
+        unfold step2_functor.
+        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 roundtrip_lemma.
+
+        apply if_inv.
+        set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
+        apply if_inv in q'.
+        eapply if_comp.
+        eapply if_comp; [ idtac | apply q' ].
+        eapply if_comp.
+        apply (if_associativity
+          (RestrictToImage r0)
+          (R' s1 s2 r0 >>>> 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 r0)
+          (R' s1 s2 r0)
+          (FullImage_InclusionFunctor _)).
+        apply (if_respects
+          (RestrictToImage r0)
+          (RestrictToImage r0)
+          (R' s1 s2 r0 >>>> FullImage_InclusionFunctor _)
+          (((R' s1 s2 r0 >>>> 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 r0)
+          (ff_functor_section_functor me_homfunctor me_full me_faithful)
+          (HomFunctor (senr_c s2) (senr_c_i s2))).
+        apply roundtrip_lemma.
+        apply if_inv.
+        apply H.
+        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; 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 *.
+      apply (eqv1 _ _ f f'); auto.
+      unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+      apply (eqv2 _ _ f f'); auto.
+      Qed.
+
 End ReificationsIsomorphicToGeneralizedArrows.