remove unproven step1_lemma (it has a proof now)

diff --git a/src/BijectionLemma.v b/src/BijectionLemma.v
new file mode 100644 (file)
index 0000000..f63cf17
--- /dev/null
+++ b/src/BijectionLemma.v
@@ -0,0 +1,71 @@
+(*********************************************************************************************************************************)
+(* Bijection Lemma                                                                                                               *)
+(*                                                                                                                               *)
+(*    Used in the proof that the mapping between the category of reifications and category of generalized arrows is in fact      *)
+(*    a functor                                                                                                                  *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+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 BijectionLemma.
+
+  (* given two categories with (for simplicity) the same objects *)
+  Context  {Obj:Type}.
+  Context  {CHom}{C:Category Obj CHom}.
+  Context  {DHom}{D:Category Obj DHom}.
+
+  (* and a functor which is (for simplicity) identity on objects *)
+  Context  {F:Functor C D (fun x => x)}.
+
+  (* and a mapping in the opposite direction, which respects equivalence *)
+  Context  {M:forall x y, (x~~{D}~~>y) -> (x~~{C}~~>y)}.
+  Implicit Arguments M [ [x] [y] ].
+  Context  {M_respects:forall x y, forall (f g:x~~{D}~~>y), f~~g -> M f ~~ M g}.
+
+  Add Parametric Morphism (x y:Obj) : (@M x y)
+  with signature ((@eqv D _ D x y) ==> (@eqv C _ C x y)) as parametric_morphism_fmor''.
+    intros; apply M_respects; auto.
+    Defined.
+
+  (*
+   * If the functor and the mapping form a bijection, then the fact
+   * that the functor preserves composition forces the mapping to do so
+   * as well
+   *)
+
+  Lemma bijection_lemma :
+    (forall A B, forall f:(A~~{C}~~>B), M (F \ f) ~~ f) ->
+    (forall A B, forall f:(A~~{D}~~>B), F \ (M f) ~~ f) ->
+    forall A B C, forall f:(A~~{D}~~>B), forall g:(B~~{D}~~>C), M f >>> M g ~~ M (f >>> g).
+  
+    intro lem1.
+    intro lem2.
+    intros.
+    rewrite <- (lem2 _ _ f).
+    rewrite <- (lem2 _ _ g).
+
+    set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q.
+    rewrite q.
+    rewrite lem1.
+    rewrite lem1.
+    rewrite lem1.
+    reflexivity.
+    Qed.
+
+End BijectionLemma.

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 1542b46..8edd1e0 100644 (file)
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -30,16 +30,10 @@ Require Import GeneralizedArrowCategory.
 Require Import ReificationCategory.
 Require Import ReificationsAndGeneralizedArrows.
 Require Import WeakFunctorCategory.
 Require Import ReificationCategory.
 Require Import ReificationsAndGeneralizedArrows.
 Require Import WeakFunctorCategory.

+Require Import BijectionLemma.

 
 Section ReificationsIsomorphicToGeneralizedArrows.
 
 
 Section ReificationsIsomorphicToGeneralizedArrows.
 

-    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 (HomFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
-      ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
-      admit.
-      Defined.
-

     Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
     Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).

@@ -157,6 +151,44 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply (garrow_from_reification s1 s2 r).
       Defined.
 
       apply (garrow_from_reification s1 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) 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:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_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) 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.
+

     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
          f ~~ f' ->
     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
          f ~~ f' ->

@@ -194,89 +226,32 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         unfold garrow_functor.
         unfold step2_functor.
         apply if_inv in H.
         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 (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
         apply if_inv.
         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).

-        apply yy'.
+        apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).

         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.
         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 >>>> HomFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
-          (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
-          (G0:=(HomFunctor s2 (mon_i s2)))
-          (G1:=(HomFunctor s2 (mon_i s2))));
-        [ idtac | apply if_id ].
-        eapply if_comp.
-        idtac.
-        apply (if_associativity (garrow_functor s1 s0 r) (HomFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
-        idtac.
-        unfold garrow_functor at 1.
-        unfold step2_functor at 1.
-        set (roundtrip_lemma'
-          (HomFunctor (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').
-        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 *.
 
     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:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor 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 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.
 
 End ReificationsIsomorphicToGeneralizedArrows.