use WeakFunctorCategory to prove GArrow/Reification isomorphism

diff --git a/src/All.v b/src/All.v
index 52bfa4a..f5e5157 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
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 (file)
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 (file)
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.
+
+