src/ReificationsIsomorphicToGeneralizedArrows.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationsIsomorphicToGeneralizedArrows:                                                                                    *)
   3 (*                                                                                                                               *)
   4 (*   The category of generalized arrows and the category of reifications are isomorphic 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 ReificationCategory.
  31 Require Import ReificationsAndGeneralizedArrows.
  32 Require Import WeakFunctorCategory.
  33 Require Import BijectionLemma.
  34
  35 Section ReificationsIsomorphicToGeneralizedArrows.
  36
  37     Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
  38       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
  39       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
  40       intro GA.
  41       destruct GA; [ apply roi_id | idtac ].
  42       apply roi_reif.
  43       apply reification_from_garrow.
  44       apply g.
  45       Defined.
  46
  47     (* I tried really hard to avoid this *)
  48     Require Import Coq.Logic.Eqdep.
  49
  50     Inductive Heq : forall {A}{B}, A -> B -> Prop :=
  51       heq : forall {A} (a:A), Heq a a.
  52
  53     Lemma invert_ga' : forall (a b: SMME)
  54       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
  55       (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
  56       intros.
  57       destruct f.
  58       left; apply heq.
  59       subst; right.
  60       exists g.
  61       apply heq.
  62       Defined.
  63
  64     Lemma invert_ga : forall (a: SMME)
  65       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
  66       (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
  67       intros.
  68       set (invert_ga' a a f (refl_equal a)) as q.
  69       destruct q.
  70       left.
  71       inversion H.
  72       apply inj_pairT2 in H2.
  73       apply inj_pairT2 in H1.
  74       subst; auto.
  75       right.
  76       destruct H.
  77       exists x.
  78       inversion H.
  79       apply inj_pairT2 in H2.
  80       apply inj_pairT2 in H1.
  81       subst; auto.
  82       Qed.
  83
  84     Lemma invert_reif' : forall (a b: SMME)
  85       (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
  86       (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
  87       intros.
  88       destruct f.
  89       left; apply heq.
  90       subst; right.
  91       exists r.
  92       apply heq.
  93       Defined.
  94
  95     Lemma invert_reif : forall (a: SMME)
  96       (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
  97       (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
  98       intros.
  99       set (invert_reif' a a f (refl_equal a)) as q.
 100       destruct q.
 101       left.
 102       inversion H.
 103       apply inj_pairT2 in H2.
 104       apply inj_pairT2 in H1.
 105       subst; auto.
 106       right.
 107       destruct H.
 108       exists x.
 109       inversion H.
 110       apply inj_pairT2 in H2.
 111       apply inj_pairT2 in H1.
 112       subst; auto.
 113       Qed.
 114
 115     Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
 116       refine {| fmor := fun a b f => M1 f |}.
 117       intros.
 118         unfold hom in *.
 119         unfold eqv in *.
 120         simpl in *.
 121         destruct f.
 122         set (invert_ga _ f') as q.
 123         destruct q; subst.
 124         apply if_id.
 125         simpl in *.
 126         destruct H0; subst.
 127         apply H.
 128         simpl in *.
 129         destruct f'; simpl in *.
 130         apply H.
 131         apply H.
 132       intros; simpl.
 133         apply if_id.
 134       intros.
 135         simpl.
 136         destruct f; simpl.
 137         apply if_id.
 138         destruct g; simpl.
 139         apply if_id.
 140         unfold mf_f; simpl.
 141         apply (if_associativity
 142           ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
 143         Defined.
 144
 145     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
 146       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
 147       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
 148       intro RE.
 149       destruct RE; [ apply gaoi_id | idtac ].
 150       apply gaoi_ga.
 151       apply (garrow_from_reification s1 s2 r).
 152       Defined.
 153
 154     Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
 155       (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
 156       (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
 157       generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
 158         unfold hom in *.
 159         set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
 160         destruct f; simpl in *.
 161         apply H.
 162         apply if_inv.
 163         apply (if_comp (if_inv H)).
 164         clear H.
 165         unfold mf_f in q.
 166         apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
 167           (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
 168         apply q.
 169         apply if_id.
 170       Qed.
 171
 172
 173     Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
 174       (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
 175       (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
 176       reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
 177         unfold hom in *.
 178         set (@roundtrip_reification_to_reification _ a _ _ b) as q.
 179         destruct f; simpl.
 180         apply H.
 181         apply if_inv.
 182         apply (if_comp (if_inv H)).
 183         clear H.
 184         simpl.
 185         unfold mf_f; simpl.
 186         simpl in q.
 187         unfold mf_f in q.
 188         simpl in q.
 189         apply q.
 190       Qed.
 191
 192     Lemma M2_respects :
 193       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
 194          f ~~ f' ->
 195          M2 a b f ~~ M2 a b f'.
 196       intros.
 197         unfold hom in *.
 198         unfold eqv in *.
 199         simpl in *.
 200         destruct f.
 201         set (invert_reif _ f') as q.
 202         destruct q; subst.
 203         apply if_id.
 204         simpl in *.
 205         destruct H0; subst.
 206         simpl in *.
 207         unfold garrow_functor.
 208         unfold step2_functor.
 209         apply (if_comp H).
 210         clear H.
 211         apply (if_comp (@step1_niso _ smme _ _ smme x)).
 212         apply if_inv.
 213         apply (@roundtrip_lemma _ smme _ _ smme x).
 214       simpl in *.
 215         destruct f'; simpl in *.
 216         apply if_inv.
 217         apply if_inv in H.
 218         apply (if_comp H).
 219         clear H.
 220         unfold garrow_functor.
 221         unfold step2_functor.
 222         apply (if_comp (@step1_niso _ smme _ _ smme r)).
 223         apply if_inv.
 224         apply (@roundtrip_lemma _ smme _ _ smme r).
 225       simpl in *.
 226         unfold garrow_functor.
 227         unfold step2_functor.
 228         apply if_inv in H.
 229         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
 230         apply if_inv.
 231         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
 232         apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
 233         Qed.
 234
 235     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
 236       refine {| fmor := fun a b f => M2 _ _ f |}.
 237       apply M2_respects.
 238       intros; simpl; apply if_id.
 239       intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
 240       apply M2_respects; auto.
 241       unfold fmor; simpl.
 242       apply (@eqv1 _ _ f0 f0).
 243       apply if_id.
 244       unfold fmor; simpl.
 245       apply (@eqv2 _ _ f0 f0).
 246       apply if_id.
 247       Defined.
 248
 249     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
 250       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
 251       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 252       apply (eqv1 _ _ f f'); auto.
 253       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 254       apply (eqv2 _ _ f f'); auto.
 255       Qed.
 256
 257 End ReificationsIsomorphicToGeneralizedArrows.