src/ReificationsIsomorphicToGeneralizedArrows.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationsEquivalentToGeneralizedArrows:                                                                                    *)
   3 (*                                                                                                                               *)
   4 (*   The category of generalized arrows and the category of reifications are equivalent categories.                              *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import Functors_ch1_4.
  13 Require Import Isomorphisms_ch1_5.
  14 Require Import ProductCategories_ch1_6_1.
  15 Require Import OppositeCategories_ch1_6_2.
  16 Require Import Enrichment_ch2_8.
  17 Require Import Subcategories_ch7_1.
  18 Require Import NaturalTransformations_ch7_4.
  19 Require Import NaturalIsomorphisms_ch7_5.
  20 Require Import MonoidalCategories_ch7_8.
  21 Require Import Coherence_ch7_8.
  22 Require Import Enrichment_ch2_8.
  23 Require Import RepresentableStructure_ch7_2.
  24 Require Import Reification.
  25 Require Import GeneralizedArrow.
  26 Require Import GeneralizedArrowFromReification.
  27 Require Import ReificationFromGeneralizedArrow.
  28 Require Import ReificationCategory.
  29 Require Import GeneralizedArrowCategory.
  30 Require Import ReificationsEquivalentToGeneralizedArrows.
  31 Require Import WeakFunctorCategory.
  32
  33 Section ReificationsIsomorphicToGeneralizedArrows.
  34
  35     Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
  36       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
  37       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
  38       intro GA.
  39       destruct GA; [ apply roi_id | idtac ].
  40       apply roi_reif.
  41       apply reification_from_garrow.
  42       apply g.
  43       Defined.
  44
  45     Lemma invert_ga : forall (a: SMME)
  46       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
  47       (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
  48       admit.
  49       Qed.
  50
  51     Lemma invert_reif : forall (a: SMME)
  52       (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
  53       (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
  54       admit.
  55       Qed.
  56
  57     Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
  58       refine {| fmor := fun a b f => M1 f |}.
  59       intros.
  60         unfold hom in *.
  61         unfold eqv in *.
  62         simpl in *.
  63         destruct f.
  64         set (invert_ga _ f') as q.
  65         destruct q; subst.
  66         apply if_id.
  67         simpl in *.
  68         destruct H0; subst.
  69         apply H.
  70         simpl in *.
  71         destruct f'; simpl in *.
  72         apply H.
  73         apply H.
  74       intros; simpl.
  75         apply if_id.
  76       intros.
  77         simpl.
  78         destruct f; simpl.
  79         apply if_id.
  80         destruct g; simpl.
  81         apply if_id.
  82         unfold mf_f; simpl.
  83         apply (if_associativity
  84           ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
  85         Defined.
  86
  87     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
  88       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
  89       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
  90       intro RE.
  91       destruct RE; [ apply gaoi_id | idtac ].
  92       apply gaoi_ga.
  93       apply (garrow_from_reification s1 s2 r).
  94       Defined.
  95
  96     Lemma M2_respects :
  97       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
  98          f ~~ f' ->
  99          M2 a b f ~~ M2 a b f'.
 100       intros.
 101         unfold hom in *.
 102         unfold eqv in *.
 103         simpl in *.
 104         destruct f.
 105         set (invert_reif _ f') as q.
 106         destruct q; subst.
 107         apply if_id.
 108         simpl in *.
 109         destruct H0; subst.
 110         simpl in *.
 111         unfold garrow_functor.
 112         unfold step2_functor.
 113         apply (if_comp H).
 114         clear H.
 115         apply (if_comp (@step1_niso _ smme _ _ smme x)).
 116         apply if_inv.
 117         apply (@roundtrip_lemma _ smme _ _ smme x).
 118       simpl in *.
 119         destruct f'; simpl in *.
 120         apply if_inv.
 121         apply if_inv in H.
 122         apply (if_comp H).
 123         clear H.
 124         unfold garrow_functor.
 125         unfold step2_functor.
 126         apply (if_comp (@step1_niso _ smme _ _ smme r)).
 127         apply if_inv.
 128         apply (@roundtrip_lemma _ smme _ _ smme r).
 129       simpl in *.
 130         unfold garrow_functor.
 131         unfold step2_functor.
 132         apply if_inv in H.
 133         set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
 134         set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
 135         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
 136         apply if_inv.
 137         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
 138         apply yy'.
 139         Qed.
 140
 141     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
 142       refine {| fmor := fun a b f => M2 _ _ f |}.
 143       apply M2_respects.
 144       intros; simpl; apply if_id.
 145       intros.
 146         simpl.
 147         destruct f; simpl.
 148         apply if_id.
 149         destruct g; simpl.
 150         apply if_id.
 151         unfold mf_f; simpl.
 152         apply (if_respects
 153           (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
 154           (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
 155           (G0:=(RepresentableFunctor s2 (mon_i s2)))
 156           (G1:=(RepresentableFunctor s2 (mon_i s2))));
 157         [ idtac | apply if_id ].
 158         admit.
 159         Defined.
 160
 161     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
 162       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
 163       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 164         unfold hom in *.
 165         set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
 166         destruct f; simpl in *.
 167         apply H.
 168         apply if_inv.
 169         apply (if_comp (if_inv H)).
 170         clear H.
 171         unfold mf_f in q.
 172         apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
 173           (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
 174         apply q.
 175         apply if_id.
 176
 177       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 178         unfold hom in *.
 179         set (@roundtrip_reification_to_reification _ a _ _ b) as q.
 180         destruct f; simpl.
 181         apply H.
 182         apply if_inv.
 183         apply (if_comp (if_inv H)).
 184         clear H.
 185         simpl.
 186         unfold mf_f; simpl.
 187         simpl in q.
 188         unfold mf_f in q.
 189         simpl in q.
 190         apply q.
 191         Qed.
 192
 193 End ReificationsIsomorphicToGeneralizedArrows.